Document Open Access Logo

Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach

Authors Alexander Bolotov, Montserrat Hermo, Paqui Lucio

PDF
Thumbnail PDF

File

LIPIcs.TIME.2018.5.pdf
  • Filesize: 0.91 MB
  • 22 pages

Document Identifiers

Author Details

Alexander Bolotov
  • University of Westminster, W1W 6UW, London, UK
Montserrat Hermo
  • University of the Basque Country, P. Manuel de Lardizabal, 1, 20018-San Sebastián, Spain
Paqui Lucio
  • University of the Basque Country, P. Manuel de Lardizabal, 1, 20018-San Sebastián, Spain

Funding

  • Bolotov, Alexander: The author would like to thank the University of Westminster for supporting the sabbatical in 2017.
  • Hermo, Montserrat: This author has been partially supported by Spanish Projects TIN2013-46181-C2-2-R and TIN2017-86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU15/30.
  • Lucio, Paqui: This author has been partially supported by Spanish Projects TIN2013-46181-C2-2-R and TIN2017-86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU15/30.

Cite As Get BibTex

Alexander Bolotov, Montserrat Hermo, and Paqui Lucio. Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.TIME.2018.5

Abstract

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 ECTL and 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 CTL^*, often considered as "the full branching-time logic" overcomes these restrictions on expressing fairness. However, this logic itself, 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 this logic, while it is known that 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. Based on these two considerations, the following problem arises - are there logics that have richer expressiveness than ECTL^+ yet "simpler" than CTL^* for which a one-pass tableau can be developed? In this paper we give a solution to this problem. We present a tree-style one-pass tableau for a sub-logic of CTL^* that we call ECTL^#, which is more expressive than ECTL^+ allowing the formulation of a new range of fairness constraints with "until" operator. The presentation of the tableau construction is accompanied by an algorithm for constructing a systematic tableau, for any given input of 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 ECTL^#, and of a dual sequent calculi.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Temporal logic
  • fairness
  • tableau
  • branching-time
  • one-pass tableau

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Therese Berg and Harald Raffelt. Model checking. In Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, and Alexander Pretschner, editors, Model-Based Testing of Reactive Systems, pages 557-603. Springer-Verlag, Berlin Heidelberg, 2005. URL: http://dx.doi.org/10.1007/b137241.
  2. Kai Brünnler and Martin Lange. Cut-free sequent systems for temporal logic. Journal of Logic and Algebraic Programming, 76(2):216-225, 2008. URL: http://dx.doi.org/10.1016/j.jlap.2008.02.004.
  3. Edmund M. Clarke, E. Allen Emerson, and Aravinda P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., 8(2):244-263, 1986. URL: http://dx.doi.org/10.1145/5397.5399.
  4. E. Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science (Vol. B), pages 995-1072. MIT Press, Cambridge, USA, 1990. URL: http://dl.acm.org/citation.cfm?id=114891.114907.
  5. E. Allen Emerson and Joseph Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences, 30(1):1-24, 1985. URL: http://dx.doi.org/10.1016/0022-0000(85)90001-7.
  6. E. Allen Emerson and Joseph Y. Halpern. Sometimes and not never revisited: On branching versus linear time temporal logic. J. ACM, 33(1):151-178, 1986. URL: http://dx.doi.org/10.1145/4904.4999.
  7. E. Allen Emerson and Chin-Laung Lei. Temporal reasoning under generalized fairness constraints. In Monien B. and Vidal-Naquet G., editors, STACS 1986, Lecture Notes in Computer Science, vol 210, pages 21-37. Springer-Verlag Berlin Heidelberg, Karlsruhe, Federal Republic of Germany, 1986. URL: http://dx.doi.org/10.1007/3-540-16078-7_62.
  8. Jose Gaintzarain, Montserrat Hermo, Paqui Lucio, Marisa Navarro, and Fernando Orejas. Dual systems of tableaux and sequents for PLTL. Journal of Logic and Algebraic Programming, 78(8):701-722, 2009. URL: http://dx.doi.org/10.1016/j.jlap.2009.05.001.
  9. Rajeev Gore. Tableau methods for modal and temporal logics. In Marcello D'Agostino, Dov M. Dov Gabbay, Reiner Hähnle, and Joachim Posegga, editors, Handbook of Tableau Methods, pages 297-396. Springer, Netherlands, Dordrecht, 1999. URL: http://dx.doi.org/10.1007/978-94-017-1754-0_6.
  10. Bernhard Josko. Model checking of ctl formulae under liveness assumptions. In Thomas Ottmann, editor, Automata, Languages and Programming, 14th International Colloquium, pages 5-24. Springer-Verlag Berlin Heidelberg, Karlsruhe, Federal Republic of Germany, 1987. URL: http://dx.doi.org/10.1007/3-540-18088-5.
  11. Jan Kretinsky and Ruslan Ledesma Garza. Rabinizer 2: Small deterministic automata for LTL$$1GU. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, pages 446-450, Heidelberg Dordrecht London New York, 2013. Springer. URL: http://dx.doi.org/10.1007/978-3-319-02444-8_32.
  12. Nicolas Markey. Temporal logics. Course notes, Master Parisien de Recherche en Informatique, Paris, France, 2013. URL: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NM-coursTL13.pdf.
  13. Mark Reynolds. A tableau for CTL^⋆. In Ana Cavalcanti and Dennis Dams, editors, FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings, volume 5850 of Lecture Notes in Computer Science, pages 403-418. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-05089-3_26.
  14. Robert S. Streett and E. Allen Emerson. The propositional mu-calculus is elementary. In Jan Paredaens, editor, Automata, Languages and Programming, 11th Colloquium, Antwerp, Belgium, July 16-20, 1984, Proceedings, volume 172 of Lecture Notes in Computer Science, pages 465-472. Springer, 1984. URL: http://dx.doi.org/10.1007/3-540-13345-3_43.
  15. Jun Sun, Yang Liu, Jin Song Dong, and Hai H. Wang. Specifying and verifying event-based fairness enhanced systems. In Shaoying Liu, Tom Maibaum, and Keijiro Araki, editors, Formal Methods and Software Engineering: 10th International Conference on Formal Engineering Methods ICFEM 2008, pages 5-24. Springer Science and Business Media, Kitakyushu-City, Japan, 2008. URL: http://dx.doi.org/10.1007/978-3-540-88194-0.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact