And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL

Rajeev Goré

doi:10.1007/978-3-319-08587-6_3

And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL

Rajeev Goré^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

12 Citations (Scopus)

Abstract

Over the last forty years, computer scientists have invented or borrowed numerous logics for reasoning about digital systems. Here, I would like to concentrate on three of them: Linear Time Temporal Logic (LTL), branching time Computation Tree temporal Logic (CTL), and Propositional Dynamic Logic (PDL), with and without converse. More specifically, I would like to present results and techniques on how to solve the satisfiability problem in these logics, with global assumptions, using the tableau method. The issues that arise are the typical tensions between computational complexity, practicality and scalability. This is joint work with Linh Anh Nguyen, Pietro Abate, Linda Postniece, Florian Widmann and Jimmy Thomson.

Original language	English
Title of host publication	Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
Publisher	Springer Verlag
Pages	26-45
Number of pages	20
ISBN (Print)	9783319085869
DOIs	https://doi.org/10.1007/978-3-319-08587-6_3
Publication status	Published - 2014
Event	7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria Duration: 19 Jul 2014 → 22 Jul 2014

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8562 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
Country/Territory	Austria
City	Vienna
Period	19/07/14 → 22/07/14

Access to Document

10.1007/978-3-319-08587-6_3

Cite this

Goré, R. (2014). And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. In Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings (pp. 26-45). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8562 LNAI). Springer Verlag. https://doi.org/10.1007/978-3-319-08587-6_3

Goré, Rajeev. / And-or tableaux for fixpoint logics with converse : LTL, CTL, PDL and CPDL. Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, 2014. pp. 26-45 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{c575fae04a61408888bed4155a8843b9,

title = "And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL",

abstract = "Over the last forty years, computer scientists have invented or borrowed numerous logics for reasoning about digital systems. Here, I would like to concentrate on three of them: Linear Time Temporal Logic (LTL), branching time Computation Tree temporal Logic (CTL), and Propositional Dynamic Logic (PDL), with and without converse. More specifically, I would like to present results and techniques on how to solve the satisfiability problem in these logics, with global assumptions, using the tableau method. The issues that arise are the typical tensions between computational complexity, practicality and scalability. This is joint work with Linh Anh Nguyen, Pietro Abate, Linda Postniece, Florian Widmann and Jimmy Thomson.",

author = "Rajeev Gor{\'e}",

year = "2014",

doi = "10.1007/978-3-319-08587-6_3",

language = "English",

isbn = "9783319085869",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "26--45",

booktitle = "Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings",

address = "Germany",

note = "7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 ; Conference date: 19-07-2014 Through 22-07-2014",

}

Goré, R 2014, And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. in Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8562 LNAI, Springer Verlag, pp. 26-45, 7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 19/07/14. https://doi.org/10.1007/978-3-319-08587-6_3

And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. / Goré, Rajeev.
Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, 2014. p. 26-45 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8562 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - And-or tableaux for fixpoint logics with converse

T2 - 7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014

AU - Goré, Rajeev

PY - 2014

Y1 - 2014

N2 - Over the last forty years, computer scientists have invented or borrowed numerous logics for reasoning about digital systems. Here, I would like to concentrate on three of them: Linear Time Temporal Logic (LTL), branching time Computation Tree temporal Logic (CTL), and Propositional Dynamic Logic (PDL), with and without converse. More specifically, I would like to present results and techniques on how to solve the satisfiability problem in these logics, with global assumptions, using the tableau method. The issues that arise are the typical tensions between computational complexity, practicality and scalability. This is joint work with Linh Anh Nguyen, Pietro Abate, Linda Postniece, Florian Widmann and Jimmy Thomson.

AB - Over the last forty years, computer scientists have invented or borrowed numerous logics for reasoning about digital systems. Here, I would like to concentrate on three of them: Linear Time Temporal Logic (LTL), branching time Computation Tree temporal Logic (CTL), and Propositional Dynamic Logic (PDL), with and without converse. More specifically, I would like to present results and techniques on how to solve the satisfiability problem in these logics, with global assumptions, using the tableau method. The issues that arise are the typical tensions between computational complexity, practicality and scalability. This is joint work with Linh Anh Nguyen, Pietro Abate, Linda Postniece, Florian Widmann and Jimmy Thomson.

UR - http://www.scopus.com/inward/record.url?scp=84958526614&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-08587-6_3

DO - 10.1007/978-3-319-08587-6_3

M3 - Conference contribution

SN - 9783319085869

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 26

EP - 45

BT - Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings

PB - Springer Verlag

Y2 - 19 July 2014 through 22 July 2014

ER -

Goré R. And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. In Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag. 2014. p. 26-45. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-08587-6_3

And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this