TY - JOUR

T1 - Inclusion dynamics hybrid automata

AU - Casagrande, Alberto

AU - Piazza, Carla

AU - Policriti, Alberto

AU - Mishra, Bud

N1 - Funding Information:
This work is partially done in the framework of the HYCON Network of Excellence, and supported by NSF’s ITR programs, DARPA’s BioCOMP/Biospice program, NYU CCPR/DHS program, PRIN’05 program 2005015491, PRIN “BISCA” 2006011235, and regional project BIOCHECK. * Corresponding author. Address: DIMI, Università di Udine, Via delle Scienze, 206, 33100 Udine, Italy. E-mail address: alberto.casagrande@dimi.uniud.it (A. Casagrande).

PY - 2008/12

Y1 - 2008/12

N2 - Hybrid systems are dynamical systems with the ability to describe mixed discrete-continuous evolution of a wide range of systems. Consequently, at first glance, hybrid systems appear powerful but recalcitrant, neither yielding to analysis and reasoning through a purely continuous-time modeling as with systems of differential equations, nor open to inferential processes commonly used for discrete state-transition systems such as finite state automata. A convenient and popular model, called hybrid automata, was introduced to model them and has spurred much interest on its tractability as a tool for inference and model checking in a general setting. Intuitively, a hybrid automaton is simply a "finite-state" automaton with each state augmented by continuous variables, which evolve according to a set of well-defined continuous laws, each specified separately for each state. This article investigates both the notion of hybrid automaton and the model checking problem over such a structure. In particular, it relates first-order theories and analysis results on multivalued maps and reduces the bounded reachability problem for hybrid automata whose continuous laws are expressed by inclusions (x ′ ∈ f (x, t)) to a decidability problem for first-order formulæ over the reals. Furthermore, the paper introduces a class of hybrid automata for which the reachability problem can be decided and shows that the problem of deciding whether a hybrid automaton belongs to this class can be again decided using first-order formulæ over the reals. Despite the fact that the bisimulation quotient for this class of hybrid automata can be infinite, we show that our techniques permit effective model checking for a nontrivial fragment of CTL.

AB - Hybrid systems are dynamical systems with the ability to describe mixed discrete-continuous evolution of a wide range of systems. Consequently, at first glance, hybrid systems appear powerful but recalcitrant, neither yielding to analysis and reasoning through a purely continuous-time modeling as with systems of differential equations, nor open to inferential processes commonly used for discrete state-transition systems such as finite state automata. A convenient and popular model, called hybrid automata, was introduced to model them and has spurred much interest on its tractability as a tool for inference and model checking in a general setting. Intuitively, a hybrid automaton is simply a "finite-state" automaton with each state augmented by continuous variables, which evolve according to a set of well-defined continuous laws, each specified separately for each state. This article investigates both the notion of hybrid automaton and the model checking problem over such a structure. In particular, it relates first-order theories and analysis results on multivalued maps and reduces the bounded reachability problem for hybrid automata whose continuous laws are expressed by inclusions (x ′ ∈ f (x, t)) to a decidability problem for first-order formulæ over the reals. Furthermore, the paper introduces a class of hybrid automata for which the reachability problem can be decided and shows that the problem of deciding whether a hybrid automaton belongs to this class can be again decided using first-order formulæ over the reals. Despite the fact that the bisimulation quotient for this class of hybrid automata can be infinite, we show that our techniques permit effective model checking for a nontrivial fragment of CTL.

KW - First-order logics over the reals

KW - Hybrid automata

KW - Model checking

UR - http://www.scopus.com/inward/record.url?scp=57649156233&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=57649156233&partnerID=8YFLogxK

U2 - 10.1016/j.ic.2008.09.001

DO - 10.1016/j.ic.2008.09.001

M3 - Article

AN - SCOPUS:57649156233

SN - 0890-5401

VL - 206

SP - 1394

EP - 1424

JO - Information and Computation

JF - Information and Computation

IS - 12

ER -