A hybrid automaton is a formal model for a system characterised by a combination of discrete and continuous components. Probabilistic hybrid automata generalise hybrid automata with the possibility of representing random behaviour of the discrete components of the system, in addition to nondeterministic choice regarding aspects such as time durations between mode switches and gradients of continuous flows. Two standard problems for probabilistic hybrid automata are verification and control: verification concerns the existence of a resolution of nondeterminism such that the resulting probability of an ω-regular property exceeds some bound; control concerns the existence of a resolution of the controllable nondeterminism, however the uncontrollable nondeterminism of the environment of the system is resolved, such that the probability of an ω-regular property exceeds some bound. While simple verification and control problems for (probabilistic) hybrid automata are in general undecidable, previous work has defined various subclasses for which the problems are decidable. In this paper, we generalise previous results by showing how bisimulation-based finite abstractions of non-probabilistic hybrid automata can be lifted to the setting of probabilistic hybrid automata. We apply these results to the subclass of probabilistic rectangular hybrid automata in a semantics in which discrete control transitions can occur only at integer points in time. These results allow us to show that, for this class of probabilistic hybrid automaton, the verification problems and control problems are decidable.

Verification and Control for Probabilistic Hybrid Automata with Finite Bisimulations

J. Sproston
2019-01-01

Abstract

A hybrid automaton is a formal model for a system characterised by a combination of discrete and continuous components. Probabilistic hybrid automata generalise hybrid automata with the possibility of representing random behaviour of the discrete components of the system, in addition to nondeterministic choice regarding aspects such as time durations between mode switches and gradients of continuous flows. Two standard problems for probabilistic hybrid automata are verification and control: verification concerns the existence of a resolution of nondeterminism such that the resulting probability of an ω-regular property exceeds some bound; control concerns the existence of a resolution of the controllable nondeterminism, however the uncontrollable nondeterminism of the environment of the system is resolved, such that the probability of an ω-regular property exceeds some bound. While simple verification and control problems for (probabilistic) hybrid automata are in general undecidable, previous work has defined various subclasses for which the problems are decidable. In this paper, we generalise previous results by showing how bisimulation-based finite abstractions of non-probabilistic hybrid automata can be lifted to the setting of probabilistic hybrid automata. We apply these results to the subclass of probabilistic rectangular hybrid automata in a semantics in which discrete control transitions can occur only at integer points in time. These results allow us to show that, for this class of probabilistic hybrid automaton, the verification problems and control problems are decidable.
2019
103
46
61
Hybrid automata, probabilistic model checking, probabilistic games
J. Sproston
File in questo prodotto:
File Dimensione Formato  
pra_post.pdf

Open Access dal 09/11/2020

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 551.33 kB
Formato Adobe PDF
551.33 kB Adobe PDF Visualizza/Apri
1-s2.0-S2352220817302262-main.pdf

Accesso riservato

Tipo di file: PDF EDITORIALE
Dimensione 781.3 kB
Formato Adobe PDF
781.3 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/1681478
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact