About: Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : wasabi.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic
Creator	Schneider, Sven Giese, Holger Maximova, Maria Sakizloglou, Lucas
Source	PMC
abstract	The nonpropositional Metric Temporal Graph Logic (MTGL) specifies the behavior of timed dynamic systems given by timed graph sequences (TGSs), which contain typed attributed graphs representing system states and the elapsed time between states. MTGL satisfaction can be analyzed for finite TGSs by translating its satisfaction problem to the satisfaction problem of nested graph conditions using a folding operation (aggregating a TGS into a graph with history) and a reduction operation (translating an MTGL condition into a nested graph condition). In this paper, we introduce an analysis procedure for MTGL to allow for an on-the-fly analysis of finite/infinite TGSs. To this end, we introduce a further (optimistic) reduction of MTGL conditions, which leads to violations during the on-the-fly analysis only when non-satisfaction is guaranteed in the future whereas the former (pessimistic) reduction leads to violations when satisfaction is not guaranteed in the future. We motivate the relevance of our analysis procedure, which uses both reduction operations, by means of a running example. Finally, we discuss prototypical support in the tool AutoGraph.
has issue date	2020-05-31(xsd:dateTime)
bibo:doi	10.1007/978-3-030-51372-6_16
has license	no-cc
sha1sum (hex)	6ad39e23da83dc9d58c6b2d8105bd075fd7652ef
schema:url	https://doi.org/10.1007/978-3-030-51372-6_16
resource representing a document's title	Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic
has PubMed Central identifier	PMC7314715
schema:publication	Graph Transformation
resource representing a document's body	covid:6ad39e23da83dc9d58c6b2d8105bd075fd7652ef#body_text
is schema:about of	named entity 'timed' named entity 'sequences' named entity 'graphs' named entity 'satisfaction' named entity 'condition' named entity 'Graph' named entity 'condition' named entity 'nested' named entity 'problem' named entity 'graph' named entity 'subset' named entity 'graph' named entity 'formal verification' named entity 'prefix relation' named entity 'computing' named entity 'satisfaction relation' named entity 'semantics' named entity 'semantics' named entity 'dts' named entity 'graph' named entity 'atomic propositions' named entity 'disjoint sets' named entity 'graph' named entity 'graph' named entity 'graph' named entity 'disjunction' named entity 'graph' named entity 'quantified variables' named entity 'parallelism' named entity 'graph' named entity 'FOL' named entity 'dts' named entity 'graph' named entity 'initial morphism' named entity 'graph' named entity 'logic' named entity 'graph' named entity 'aabb' named entity 'static analysis' named entity 'graph' named entity 'morphism' named entity 'graph' named entity 'semantics' named entity 'graph' named entity 'formal specification' named entity 'high level' named entity 'injective' named entity 'real-time' named entity 'upper bound' named entity 'dts' named entity 'initial morphism' named entity 'host graph' named entity 'offline analysis' named entity 'Gta' named entity 'G i' named entity 'G 3' named entity 'predicate' named entity 'semantics' named entity 'graph' named entity 'pattern matching' named entity 'morphism' named entity 'graph' named entity 'syntactic' named entity 'partial function' named entity 'graph' named entity 'graph' named entity 'subgraph' named entity 'number of elements' named entity 'satisfaction relation' named entity 'graph' named entity 'satisfaction relation' named entity 'graph' named entity 'lower bound' named entity 'graph' named entity 'Morphisms' named entity 'graph' named entity 'graph' named entity 'formal parameter' named entity 'graph' named entity 'dynamic systems'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software