A Fragment of Linear Temporal Logic for Universal Very Weak Automata
Many temporal specifications used in practical model checking can be represented as universal very weak automata (UVW). They are structurally simple and their states can be labeled by simple temporal logic formulas that they represent. For complex temporal properties, it can be hard to understand why a trace violates a property, so when employing UVWs in model checking, this information helps with interpreting the trace. At the same time, the simple structure of UVWs helps the model checker with finding short traces.
While a translation from computation tree logic (CTL) with only universal path quantifiers to UVWs has been described in earlier work, complex temporal properties that define sequences of allowed events along computations of a system are easier to describe in linear temporal logic (LTL). However, no direct translation from LTL to UVWs with little blow-up is known.
In this paper, we define a fragment of LTL that gives rise to a simple and efficient translation from it to UVW. The logic contains the most common shapes of safety and liveness properties, including all nestings of “Until”-subformulas. We give a translation from this fragment to UVWs that only has an exponential blow-up in the worst case, which we show to be unavoidable. We demonstrate that the simple shape of UVWs helps with understanding counter-examples in a case study.
- 1.Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE FOCS, pp. 46–57 (1977)Google Scholar
- 2.Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
- 3.Blahoudek, F., Duret-Lutz, A., Kretínský, M., Strejcek, J.: Is there a best Büchi automaton for explicit model checking? In: SPIN Symposium, pp. 68–76 (2014)Google Scholar
- 5.Basin, D., Bhatt, B.N., Traytel, D.: Optimal proofs for linear temporal logic on lasso words. In: 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018) (2018)Google Scholar
- 6.Maidl, M.: The common fragment of CTL and LTL. In: Proceedings of the 41st Annual Symposium on Foundations of Computer Science (FOCS), pp. 643–652 (2000)Google Scholar
- 8.Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Menlo Park (2004)Google Scholar
- 9.Cichon, J., Czubak, A., Jasinski, A.: Minimal Büchi automata for certain classes of LTL formulas. In: Fourth International Conference on Dependability of Computer Systems, (DepCos-RELCOMEX), pp. 17–24 (2009)Google Scholar
- 16.Kamel, M., Leue, S.: Validation of a remote object invocation and object migration in CORBA GIOP using Promela/Spin. In: International SPIN Workshop (1998)Google Scholar