×

Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\). (English) Zbl 1433.03049

Summary: Temporal logic has become essential for various areas in computer science, most notably for the specification and verification of hardware and software systems. For the specification purposes rich temporal languages are required that, in particular, can express fairness constraints. For linear-time logics which deal with fairness in the linear-time setting, one-pass and two-pass tableau methods have been developed. In the repository of the CTL-type branching-time setting, the well-known logics \(\mathsf{ECTL}\) and \(\mathsf{ECTL}^+\) were developed to explicitly deal with fairness. However, due to the syntactical restrictions, these logics can only express restricted versions of fairness. The logic \(\mathsf{CTL}^\star \), often considered as ‘the full branching-time logic’ overcomes these restrictions on expressing fairness. However, \( \mathsf{CTL}^\star\) is extremely challenging for the application of verification techniques, and the tableau technique, in particular. For example, there is no one-pass tableau construction for \(\mathsf{CTL}^\star \), while one-pass tableau has an additional benefit enabling the formulation of dual sequent calculi that are often treated as more ‘natural’ being more friendly for human understanding. These two considerations lead to the following problem - are there logics that have richer expressiveness than \(\mathsf{ECTL}^+\), allowing the formulation of a new range of fairness constraints with ‘until’ operator, yet ‘simpler’ than \(\mathsf{CTL}^\star \), and for which a one-pass tableau can be developed? Here we give a positive answer to this question, introducing a sub-logic of \(\mathsf{CTL}^\star\) called \(\mathsf{ECTL}^{\#} \), its tree-style one-pass tableau, and an algorithm for obtaining a systematic tableau, for any given admissible branching-time formulae. We prove the termination, soundness and completeness of the method. As tree-shaped one-pass tableaux are well suited for the automation and are amenable for the implementation and for the formulation of sequent calculi. Our results also open a prospect of relevant developments of the automation and implementation of the tableau method for \(\mathsf{ECTL}^{\#} \), and of a dual sequent calculi.

MSC:

03B44 Temporal logic
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

TTM; Rabinizer
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Emerson, E. A.; Halpern, J. Y., Decision procedures and expressiveness in the temporal logic of branching time, J. Comput. Syst. Sci., 30, 1, 1-24 (1985) · Zbl 0559.68051
[2] Emerson, E. A.; Halpern, J. Y., Sometimes and not never revisited: on branching versus linear time temporal logic, J. ACM, 33, 1, 151-178 (1986) · Zbl 0629.68020
[3] Clarke, E. M.; Emerson, E. A.; Sistla, A. P., Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst., 8, 2, 244-263 (1986) · Zbl 0591.68027
[4] Josko, B., Model checking of ctl formulae under liveness assumptions, (Ottmann, T., Automata, Languages and Programming, 14th International Colloquium (1987), Springer-Verlag Berlin Heidelberg: Springer-Verlag Berlin Heidelberg Karlsruhe), 5-24, Federal Republic of Germany · Zbl 0623.68030
[5] Emerson, E. A.; Lei, C.-L., Temporal reasoning under generalized fairness constraints, (Monien, B.; Vidal-Naquet, G., STACS 1986. STACS 1986, Lecture Notes in Computer Science, vol. 210 (1986), Springer-Verlag Berlin Heidelberg: Springer-Verlag Berlin Heidelberg Karlsruhe), 21-37, Federal Republic of Germany · Zbl 0614.03023
[6] Berg, T.; Raffelt, H., Model checking, (Broy, M.; Jonsson, B.; Katoen, J.-P.; Leucker, M.; Pretschner, A., Model-Based Testing of Reactive Systems (2005), Springer-Verlag: Springer-Verlag Berlin Heidelberg), 557-603 · Zbl 1070.68088
[7] Sun, J.; Liu, Y.; Dong, J. S.; Wang, H. H., Specifying and verifying event-based fairness enhanced systems, (Liu, S.; Maibaum, T.; Araki, K., Formal Methods and Software Engineering: 10th International Conference on Formal Engineering Methods ICFEM 2008 (2008), Springer Science and Business Media: Springer Science and Business Media Kitakyushu-City, Japan), 5-24
[8] Kretinsky, J.; Ledesma Garza, R., Rabinizer 2: Small deterministic automata for LTL\GU, (Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013 (2013), Springer: Springer Heidelberg Dordrecht London New York), 446-450 · Zbl 1410.68231
[9] Emerson, E. A., Temporal and modal logic, (van Leeuwen, J., Handbook of Theoretical Computer Science (Vol. B) (1990), MIT Press: MIT Press Cambridge, USA), 995-1072 · Zbl 0900.03030
[10] Markey, N., Temporal logics, course notes (2013), Master Parisien de Recherche en Informatique, Paris, France
[11] Brünnler, K.; Lange, M., Cut-free sequent systems for temporal logic, J. Log. Algebraic Program., 76, 2, 216-225 (2008) · Zbl 1151.03009
[12] Gaintzarain, J.; Hermo, M.; Lucio, P.; Navarro, M.; Orejas, F., Dual systems of tableaux and sequents for \(\mathsf{PLTL} \), J. Log. Algebraic Program., 78, 8, 701-722 (2009) · Zbl 1183.68596
[13] Abate, P.; Goré, R.; Widmann, F., One-pass tableaux for computation tree logic, (Dershowitz, N.; Voronkov, A., Logic for Programming, Artificial Intelligence, and Reasoning (2007), Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg), 32-46 · Zbl 1137.03304
[14] Friedmann, O.; Latte, M.; Lange, M., A decision procedure for CTL* based on tableaux and automata, (Giesl, J.; Hähnle, R., Automated Reasoning (2010), Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg), 331-345 · Zbl 1257.03035
[15] Pnueli, A.; Kesten, Y., A deductive proof system for CTL*, (Brim, L.; Křetínský, M.; Kučera, A.; Jančar, P., CONCUR 2002 — Concurrency Theory (2002), Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg), 24-40 · Zbl 1012.68119
[16] MaCabe-Dansted, J. C.; Reynolds, M., Rewrite rules for CTL*, J. Appl. Log., 21, 24-56 (2017) · Zbl 1436.03124
[17] Reynolds, M., A tableau for CTL^⋆, (Cavalcanti, A.; Dams, D., Proceedings. FM 2009: Formal Methods, Second World Congress. Proceedings. FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings. FM 2009: Formal Methods, Second World Congress. Proceedings. FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009, Lecture Notes in Computer Science, vol. 5850 (2009), Springer), 403-418 · Zbl 1175.68007
[18] Reynolds, M., A tableau-based decision procedure for CTL*, Form. Asp. Comput., 23, 6, 739-779 (2011) · Zbl 1242.68302
[19] Cerrito, S.; David, A.; Goranko, V., Optimal Tableau Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-Time Temporal Logic ATL+, vol. 17 (2014)
[20] Gore, R., Tableau methods for modal and temporal logics, (D’Agostino, M.; Dov Gabbay, D. M.; Hähnle, R.; Posegga, J., Handbook of Tableau Methods (1999), Springer: Springer Netherlands, Dordrecht), 297-396 · Zbl 0972.03529
[21] Bolotov, A.; Hermo, M.; Lucio, P., Extending fairness expressibility of ECTL+: a tree-style one-pass tableau approach, (Alechina, N.; Nørvåg, K.; Penczek, W., 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). 25th International Symposium on Temporal Representation and Reasoning (TIME 2018), Leibniz International Proceedings in Informatics (LIPIcs), vol. 120 (2018), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik), Article 5 pp. · Zbl 1487.68154
[22] Streett, R. S.; Emerson, E. A., The propositional mu-calculus is elementary, (Paredaens, J., Automata, Languages and Programming. Proceedings. Automata, Languages and Programming. Proceedings, 11th Colloquium, Antwerp, Belgium, July 16-20, 1984. Automata, Languages and Programming. Proceedings. Automata, Languages and Programming. Proceedings, 11th Colloquium, Antwerp, Belgium, July 16-20, 1984, Lecture Notes in Computer Science, vol. 172 (1984), Springer), 465-472 · Zbl 0556.68005
[23] Kupferman, O.; Vardi, M. Y.; Wolper, P., An automata-theoretic approach to branching-time model checking, J. ACM, 47, 2, 312-360 (2000) · Zbl 1133.68376
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.