An Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability

Rajeev Goré; Florian Widmann

doi:10.1007/978-3-642-02959-2_32

An Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability

Rajeev Goré^*, Florian Widmann

^*Corresponding author for this work

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

22 Citations (Scopus)

Abstract

We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic. Our main contribution is a sound method to track unfulfilled eventualities "on the fly" which allows us to detect "bad loops" sooner rather than in multiple subsequent passes. We achieve this by propagating and updating the "status" of nodes throughout the underlying graph as soon as is possible. We give sufficient details to enable an easy implementation by others. Preliminary experimental results from our unoptimised OCaml implementation indicate that our algorithm is feasible.

Original language	English
Title of host publication	Proceedings of the 22nd International Conference on Automated Deduction
Editors	R A Schmidt
Place of Publication	berlin
Publisher	Springer
Pages	437-452
Number of pages	16
Edition	Peer Reviewed
ISBN (Print)	3642029582, 9783642029585
DOIs	https://doi.org/10.1007/978-3-642-02959-2_32 https://doi.org/10.1007/978-3-642-02959-2_32
Publication status	Published - 2009
Event	International Conference on Automated Deduction (CADE 2009) - Montreal Canada Duration: 1 Jan 2009 → … http://www.springerlink.com/content/978-3-642-02958-5/

Publication series

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

Conference

Conference	International Conference on Automated Deduction (CADE 2009)
Period	1/01/09 → …
Other	August 2-7 2009
Internet address	http://www.springerlink.com/content/978-3-642-02958-5/

Access to Document

Cite this

Goré, R., & Widmann, F. (2009). An Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability. In R. A. S. (Ed.), Proceedings of the 22nd International Conference on Automated Deduction (Peer Reviewed ed., pp. 437-452). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5663 LNAI). Springer. https://doi.org/10.1007/978-3-642-02959-2_32, https://doi.org/10.1007/978-3-642-02959-2_32

Goré, Rajeev ; Widmann, Florian. / An Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability. Proceedings of the 22nd International Conference on Automated Deduction. editor / R A Schmidt. Peer Reviewed. ed. berlin : Springer, 2009. pp. 437-452 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{649afe466ac84fd588878204cda4ebc4,

title = "An Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability",

abstract = "We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic. Our main contribution is a sound method to track unfulfilled eventualities {"}on the fly{"} which allows us to detect {"}bad loops{"} sooner rather than in multiple subsequent passes. We achieve this by propagating and updating the {"}status{"} of nodes throughout the underlying graph as soon as is possible. We give sufficient details to enable an easy implementation by others. Preliminary experimental results from our unoptimised OCaml implementation indicate that our algorithm is feasible.",

author = "Rajeev Gor{\'e} and Florian Widmann",

year = "2009",

doi = "10.1007/978-3-642-02959-2_32",

language = "English",

isbn = "3642029582",

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

publisher = "Springer",

pages = "437--452",

editor = "{R A Schmidt}",

booktitle = "Proceedings of the 22nd International Conference on Automated Deduction",

edition = "Peer Reviewed",

note = "International Conference on Automated Deduction (CADE 2009) ; Conference date: 01-01-2009",

url = "http://www.springerlink.com/content/978-3-642-02958-5/",

}

Goré, R & Widmann, F 2009, An Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability. in RAS (ed.), Proceedings of the 22nd International Conference on Automated Deduction. Peer Reviewed edn, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5663 LNAI, Springer, berlin, pp. 437-452, International Conference on Automated Deduction (CADE 2009), 1/01/09. https://doi.org/10.1007/978-3-642-02959-2_32, https://doi.org/10.1007/978-3-642-02959-2_32

An Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability. / Goré, Rajeev; Widmann, Florian.
Proceedings of the 22nd International Conference on Automated Deduction. ed. / R A Schmidt. Peer Reviewed. ed. berlin: Springer, 2009. p. 437-452 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5663 LNAI).

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

TY - GEN

T1 - An Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability

AU - Goré, Rajeev

AU - Widmann, Florian

PY - 2009

Y1 - 2009

N2 - We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic. Our main contribution is a sound method to track unfulfilled eventualities "on the fly" which allows us to detect "bad loops" sooner rather than in multiple subsequent passes. We achieve this by propagating and updating the "status" of nodes throughout the underlying graph as soon as is possible. We give sufficient details to enable an easy implementation by others. Preliminary experimental results from our unoptimised OCaml implementation indicate that our algorithm is feasible.

AB - We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic. Our main contribution is a sound method to track unfulfilled eventualities "on the fly" which allows us to detect "bad loops" sooner rather than in multiple subsequent passes. We achieve this by propagating and updating the "status" of nodes throughout the underlying graph as soon as is possible. We give sufficient details to enable an easy implementation by others. Preliminary experimental results from our unoptimised OCaml implementation indicate that our algorithm is feasible.

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

U2 - 10.1007/978-3-642-02959-2_32

DO - 10.1007/978-3-642-02959-2_32

M3 - Conference contribution

SN - 3642029582

SN - 9783642029585

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

SP - 437

EP - 452

BT - Proceedings of the 22nd International Conference on Automated Deduction

A2 - null, R A Schmidt

PB - Springer

CY - berlin

T2 - International Conference on Automated Deduction (CADE 2009)

Y2 - 1 January 2009

ER -

Goré R, Widmann F. An Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability. In RAS, editor, Proceedings of the 22nd International Conference on Automated Deduction. Peer Reviewed ed. berlin: Springer. 2009. p. 437-452. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-02959-2_32, 10.1007/978-3-642-02959-2_32

An Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this