In finite-state systems, true existential properties admit witnesses in form of lasso-shaped fair paths. When dealing with the infinite-state case (e.g. software non-termination, model checking of hybrid automata) this is no longer the case. In this paper, we propose a compositional approach for proving the existence of fair paths of infinite-state systems. First, we describe a formal approach to prove the existence of a non-empty under-approximation of the original system that only contains fair paths. Second, we define an automated procedure that, given a set of hints (in form of basic components), searches for a suitable composition proving the existence of a fair path. We experimentally evaluate the approach on examples taken from both software and hybrid systems, showing its wide applicability and expressiveness.

Proving the Existence of Fair Paths in Infinite-State Systems / Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico. - 12597:(2021), pp. 104-126. (Intervento presentato al convegno Verification, Model Checking, and Abstract Interpretation, VMCAI 2021 tenutosi a Copenhagen, Denmark nel 17th January - 19th January 2021) [10.1007/978-3-030-67067-2_6].

Proving the Existence of Fair Paths in Infinite-State Systems

Cimatti, Alessandro;Griggio, Alberto;Magnago, Enrico
2021-01-01

Abstract

In finite-state systems, true existential properties admit witnesses in form of lasso-shaped fair paths. When dealing with the infinite-state case (e.g. software non-termination, model checking of hybrid automata) this is no longer the case. In this paper, we propose a compositional approach for proving the existence of fair paths of infinite-state systems. First, we describe a formal approach to prove the existence of a non-empty under-approximation of the original system that only contains fair paths. Second, we define an automated procedure that, given a set of hints (in form of basic components), searches for a suitable composition proving the existence of a fair path. We experimentally evaluate the approach on examples taken from both software and hybrid systems, showing its wide applicability and expressiveness.
2021
Verification, Model Checking, and Abstract Interpretation: 22nd International Conference, VMCAI 2021
USA
SPRINGER
978-3-030-67066-5
978-3-030-67067-2
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico
Proving the Existence of Fair Paths in Infinite-State Systems / Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico. - 12597:(2021), pp. 104-126. (Intervento presentato al convegno Verification, Model Checking, and Abstract Interpretation, VMCAI 2021 tenutosi a Copenhagen, Denmark nel 17th January - 19th January 2021) [10.1007/978-3-030-67067-2_6].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11572/296025
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact