Temporal prophecy for proving temporal properties of infinite-state systems
| Autor: | Jochen Hoenicke, Andreas Podelski, Sharon Shoham, Kenneth L. McMillan, Mooly Sagiv, Oded Padon |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
060201 languages & linguistics
FOS: Computer and information sciences Computer Science - Logic in Computer Science Property (programming) Cut-elimination theorem Computer science Verification system 020207 software engineering 06 humanities and the arts 02 engineering and technology Logic in Computer Science (cs.LO) 020202 computer hardware & architecture Theoretical Computer Science Safety property Transformation (function) Linear temporal logic Hardware and Architecture Robustness (computer science) Computer Science::Logic in Computer Science 0602 languages and literature 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing State (computer science) Algorithm Software |
| Zdroj: | 2018 Formal Methods in Computer Aided Design (FMCAD) FMCAD |
| ISSN: | 1572-8102 0925-9856 |
| DOI: | 10.1007/s10703-021-00377-1 |
| Popis: | Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imprecise. That is, for some instances, the temporal property holds, but the resulting safety property does not. This paper introduces a mechanism for tackling this imprecision. This mechanism, which we call temporal prophecy, is inspired by prophecy variables. Temporal prophecy refines an infinite-state system using first-order linear temporal logic formulas, via a suitable tableau construction. For a specific liveness-to-safety transformation based on first-order logic, we show that using temporal prophecy strictly increases the precision. Furthermore, temporal prophecy leads to robustness of the proof method, which is manifested by a cut elimination theorem. We integrate our approach into the Ivy deductive verification system, and show that it can handle challenging temporal verification examples. 11 pages, presented at FMCAD 2018 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink