Inclusion dynamics hybrid automata

Alberto Casagrande, Carla Piazza, Alberto Policriti, Bhubaneswar Mishra

Research output: Contribution to journalArticle

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 languageEnglish (US)
Pages (from-to)1394-1424
Number of pages31
JournalInformation and Computation
Volume206
Issue number12
DOIs
StatePublished - Dec 2008

Fingerprint

Hybrid Automata
Model checking
Inclusion
Finite automata
Hybrid systems
Computability and decidability
Model Checking
Finite State Automata
First-order
Reachability
Hybrid Systems
Dynamical systems
Differential equations
Multivalued Map
Tractability
Bisimulation
Transition Systems
Continuous Variables
State Transition
Decidability

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

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

In: Information and Computation, Vol. 206, No. 12, 12.2008, p. 1394-1424.

Research output: Contribution to journalArticle

Casagrande, A, Piazza, C, Policriti, A & Mishra, B 2008, 'Inclusion dynamics hybrid automata', Information and Computation, vol. 206, no. 12, pp. 1394-1424. https://doi.org/10.1016/j.ic.2008.09.001
Casagrande, Alberto ; Piazza, Carla ; Policriti, Alberto ; Mishra, Bhubaneswar. / Inclusion dynamics hybrid automata. In: Information and Computation. 2008 ; Vol. 206, No. 12. pp. 1394-1424.
@article{bb331fba54f548a8b85ca3b7f862754e,
title = "Inclusion dynamics hybrid automata",
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{\ae} 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{\ae} 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.",
keywords = "First-order logics over the reals, Hybrid automata, Model checking",
author = "Alberto Casagrande and Carla Piazza and Alberto Policriti and Bhubaneswar Mishra",
year = "2008",
month = "12",
doi = "10.1016/j.ic.2008.09.001",
language = "English (US)",
volume = "206",
pages = "1394--1424",
journal = "Information and Computation",
issn = "0890-5401",
publisher = "Elsevier Inc.",
number = "12",

}

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 -