### Abstract

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.

Original language | English (US) |
---|---|

Pages (from-to) | 1394-1424 |

Number of pages | 31 |

Journal | Information and Computation |

Volume | 206 |

Issue number | 12 |

DOIs | |

State | Published - Dec 2008 |

### Fingerprint

### Keywords

- First-order logics over the reals
- Hybrid automata
- Model checking

### ASJC Scopus subject areas

- Information Systems
- Computational Theory and Mathematics
- Theoretical Computer Science
- Computer Science Applications

### Cite this

*Information and Computation*,

*206*(12), 1394-1424. https://doi.org/10.1016/j.ic.2008.09.001

**Inclusion dynamics hybrid automata.** / Casagrande, Alberto; Piazza, Carla; Policriti, Alberto; Mishra, Bhubaneswar.

Research output: Contribution to journal › Article

*Information and Computation*, vol. 206, no. 12, pp. 1394-1424. https://doi.org/10.1016/j.ic.2008.09.001

}

TY - JOUR

T1 - Inclusion dynamics hybrid automata

AU - Casagrande, Alberto

AU - Piazza, Carla

AU - Policriti, Alberto

AU - Mishra, Bhubaneswar

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

VL - 206

SP - 1394

EP - 1424

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 12

ER -