Hybrid automata provide a modeling formalism for systems characterized by a combination of discrete and continuous components. Probabilistic rectangular automata generalize the class of rectangular hybrid automata with the possibility of representing random behavior of the discrete components of the system. We consider the following two problems regarding probabilistic rectangular automata: verification concerns the computation of the maximum probability with which the system can satisfy a certain omega-regular specification, control concerns the computation of a strategy which guides certain choices of the system in order to maximize the probability of satisfying a certain omega-regular specification. Our main contribution is to give algorithms for the verification and control problems for probabilistic rectangular automata in a semantics in which discrete control transitions can occur only at integer points in time. Additionally, we give algorithms for verification of omega-regular specifications of probabilistic timed automata, a subclass of probabilistic rectangular automata, with the usual dense-time semantics.

Discrete-Time Verification and Control for Probabilistic Rectangular Hybrid Automata

SPROSTON, Jeremy James
2011-01-01

Abstract

Hybrid automata provide a modeling formalism for systems characterized by a combination of discrete and continuous components. Probabilistic rectangular automata generalize the class of rectangular hybrid automata with the possibility of representing random behavior of the discrete components of the system. We consider the following two problems regarding probabilistic rectangular automata: verification concerns the computation of the maximum probability with which the system can satisfy a certain omega-regular specification, control concerns the computation of a strategy which guides certain choices of the system in order to maximize the probability of satisfying a certain omega-regular specification. Our main contribution is to give algorithms for the verification and control problems for probabilistic rectangular automata in a semantics in which discrete control transitions can occur only at integer points in time. Additionally, we give algorithms for verification of omega-regular specifications of probabilistic timed automata, a subclass of probabilistic rectangular automata, with the usual dense-time semantics.
2011
8th International Conference on Quantitative Evaluation of Systems (QEST 2011)
Aachen, Germany
5/09/2011 - 8/09/2011
Proceedings of the 8th International Conference on Quantitative Evaluation of Systems (QEST 2011)
IEEE Computer Society Press
79
88
9781457709739
Hybrid automata, probabilistic model checking
J. SPROSTON
File in questo prodotto:
File Dimensione Formato  
qest11_4aperto.pdf

Accesso aperto

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 367.24 kB
Formato Adobe PDF
367.24 kB Adobe PDF Visualizza/Apri

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/123771
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 19
  • ???jsp.display-item.citation.isi??? ND
social impact