We present a fully-symbolic LTL model checking approach for infinite-state transition systems. We extend liveness-to-safety, a prominent approach in the finite-state case, by means of implicit abstraction, to effectively prove the absence of abstract fair loops without explicitly constructing the abstract state space. We increase the effectiveness of the approach by integrating termination techniques based on well-founded relations derived from ranking functions. The idea is to prove that any existing abstract fair loop is covered by a given set of well-founded relations. Within this framework, kk-liveness is integrated as a generic ranking function. The algorithm iterates by attempting to remove spurious abstract fair loops: either it finds new predicates, to avoid spurious abstract prefixes, or it introduces new well-founded relations, based on the analysis of the abstract lasso. The implementation fully leverages the efficiency and incrementality of the underlying safety checker IC3ia. The proposed approach outperforms other temporal checkers on a wide class of benchmarks.

Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations / Jakub, Daniel; Cimatti, Alessandro; Griggio, Alberto; Tonetta, Stefano; Mover, Sergio. - 9779:(2016), pp. 271-291. (Intervento presentato al convegno 28th International Conference on Computer Aided Verification, CAV 2016 tenutosi a Toronto, Canada nel July 17-23, 2016) [10.1007/978-3-319-41528-4_15].

Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations

Cimatti, Alessandro;Griggio, Alberto;Tonetta, Stefano;Mover, Sergio
2016-01-01

Abstract

We present a fully-symbolic LTL model checking approach for infinite-state transition systems. We extend liveness-to-safety, a prominent approach in the finite-state case, by means of implicit abstraction, to effectively prove the absence of abstract fair loops without explicitly constructing the abstract state space. We increase the effectiveness of the approach by integrating termination techniques based on well-founded relations derived from ranking functions. The idea is to prove that any existing abstract fair loop is covered by a given set of well-founded relations. Within this framework, kk-liveness is integrated as a generic ranking function. The algorithm iterates by attempting to remove spurious abstract fair loops: either it finds new predicates, to avoid spurious abstract prefixes, or it introduces new well-founded relations, based on the analysis of the abstract lasso. The implementation fully leverages the efficiency and incrementality of the underlying safety checker IC3ia. The proposed approach outperforms other temporal checkers on a wide class of benchmarks.
2016
Computer Aided Verification - 28th International Conference, CAV 2016
Cham, Switzerland
Springer
978-3-319-41527-7
Jakub, Daniel; Cimatti, Alessandro; Griggio, Alberto; Tonetta, Stefano; Mover, Sergio
Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations / Jakub, Daniel; Cimatti, Alessandro; Griggio, Alberto; Tonetta, Stefano; Mover, Sergio. - 9779:(2016), pp. 271-291. (Intervento presentato al convegno 28th International Conference on Computer Aided Verification, CAV 2016 tenutosi a Toronto, Canada nel July 17-23, 2016) [10.1007/978-3-319-41528-4_15].
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/343000
 Attenzione

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

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