Verification of infinite-state dynamic systems using approximate quotient transition systems

DOI10.1109/9.948467zbMath1031.93123OpenAlexW2105826449MaRDI QIDQ4540483

Alongkrit Chutinan, Bruce H. Krogh

Publication date: 21 July 2002

Published in: IEEE Transactions on Automatic Control (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/230d5cc8a374e9a1f27ee51eb98a5e1ed3840015

zbMATH Keywords

verificationhybrid systemsreachabilitybisimulationtemporal logictransition systemscomputation tree logicapproximate quotient transition system

Mathematics Subject Classification ID

Discrete event control/observation systems (93C65) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Attainable sets, reachability (93B03)

Related Items

A deductive approach towards reasoning about algebraic transition systems, On quotients of Boolean control networks, Compositional abstraction refinement for control synthesis, A framework for multi-robot motion planning from temporal logic specifications, Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems, Abstractions for hybrid systems, CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks, Hybrid abstractions of affine systems, Control-invariance of hybrid systems with forcible events, Probabilistic model checking of biological systems with uncertain kinetic rates