About: The behavior of various kinds of dynamic systems can be formalized using typed attributed graph transformation systems (GTSs). The states of these systems are then modelled using graphs and the evolution of the system from one state to another is described by a finite set of graph transformation rules. GTSs with small finite state spaces can be analyzed with ease but analysis is intractable/undecidable for GTSs inducing large/infinite state spaces due to the inherent expressiveness of GTSs. Hence, automatic analysis procedures do not terminate or return indefinite or incorrect results. We propose an analysis procedure for establishing state-invariants for GTSs that are given by nested graph conditions (GCs). To this end, we formalize a symbolic analysis algorithm based on k-induction using Isabelle, apply it to GTSs and GCs over typed attributed graphs, develop support to single out some spurious counterexamples, and demonstrate the feasibility of the approach using our prototypical implementation.   Goto Sponge  NotDistinct  Permalink

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

AttributesValues
type
value
  • The behavior of various kinds of dynamic systems can be formalized using typed attributed graph transformation systems (GTSs). The states of these systems are then modelled using graphs and the evolution of the system from one state to another is described by a finite set of graph transformation rules. GTSs with small finite state spaces can be analyzed with ease but analysis is intractable/undecidable for GTSs inducing large/infinite state spaces due to the inherent expressiveness of GTSs. Hence, automatic analysis procedures do not terminate or return indefinite or incorrect results. We propose an analysis procedure for establishing state-invariants for GTSs that are given by nested graph conditions (GCs). To this end, we formalize a symbolic analysis algorithm based on k-induction using Isabelle, apply it to GTSs and GCs over typed attributed graphs, develop support to single out some spurious counterexamples, and demonstrate the feasibility of the approach using our prototypical implementation.
Subject
  • Mathematical modeling
  • Mathematical and quantitative methods (economics)
  • Systems theory
  • Time series models
  • Basic concepts in set theory
  • Dynamical systems
  • Cardinal numbers
  • Physical systems
  • Computability theory
  • Time domain analysis
  • Logic in computer science
  • Graph rewriting
  • Undecidable problems
  • Classical control theory
part of
is abstract of
is hasSource of
Faceted Search & Find service v1.13.91 as of Mar 24 2020


Alternative Linked Data Documents: Sponger | ODE     Content Formats:       RDF       ODATA       Microdata      About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data]
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