Name
Abstract | ||
|---|---|---|
We call a linear time property simple if counterexamples are accepted by a Büchi automaton that has only singleton strongly connected components. This class contains interesting properties such as LTL formulas $G(\varphi \implies F \psi)$ or ϕU ψ which have not yet received support beyond general LTL preserving approaches. We contribute a stubborn set approach to simple properties with the following ingredients. First, we decompose the verification problem into finitely many simpler problems that can be independently executed. Second, we propose a stubborn set method for the resulting problems that does neither require cycle detection, nor stuttering invariance, nor existence of transitions that are invisible to all atomic propositions. This means that our approach is applicable in cases where traditional approaches fail. Third, we show that sufficient potential is left in existing implementations of the proposed conditions by exploiting all the available nondeterminism in these procedures. We employ a translation to integer linear programming (ILP) for supporting this claim. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-31131-4_13 | Petri Nets |
Keywords | Field | DocType |
simple linear time property,traditional approach,general ltl,stubborn set approach,linear time property simple,available nondeterminism,linear programming,atomic proposition,simple property,ltl formula,stubborn set method | Discrete mathematics,Invariant (physics),Computer science,Atomic sentence,Cycle detection,Integer programming,Counterexample,Strongly connected component,Time complexity,Büchi automaton | Conference |
Citations | PageRank | References |
3 | 0.37 | 18 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andreas Lehmann | 1 | 3 | 0.37 |
| Niels Lohmann | 2 | 999 | 49.45 |
| Karsten Wolf | 3 | 757 | 42.53 |