PDL over Accelerated Labeled Transition Systems

T. Chen, Jan Cornelis van de Pol, Yanjing Wang

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)
    36 Downloads (Pure)

    Abstract

    We present a thorough study of Propositional Dynamic Logic over a variation of labeled transition systems, called accelerated labelled transition systems, which are transition systems labeled with regular expressions over action labels. We study the model checking and satisfiability decision problems. Through a notion of regular expression rewriting, we reduce these two problems to the corresponding ones of PDL in the traditional semantics (w.r.t. LTS). As for the complexity, both of problems are proved to be Expspace-complete. Moreover, the program complexity of model checking problem turns out to be Nlogspace-complete. Furthermore, we provide an axiomatization for PDL which involves Kleene Algebra as an Oracle. The soundness and completeness are shown.
    Original languageUndefined
    Title of host publication2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering
    Place of PublicationLos Alamitos
    PublisherIEEE Computer Society
    Pages193-200
    Number of pages8
    ISBN (Print)978-0-7695-3249-3
    DOIs
    Publication statusPublished - Jun 2008
    Event2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008 - Nanjing, China
    Duration: 17 Jun 200819 Jun 2008
    Conference number: 2

    Publication series

    Name
    PublisherIEEE Computer Society Press
    Number302

    Conference

    Conference2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008
    Abbreviated titleTASE
    CountryChina
    CityNanjing
    Period17/06/0819/06/08

    Keywords

    • EWI-12952
    • METIS-251038
    • IR-64837
    • CR-F.3.1

    Cite this

    Chen, T., van de Pol, J. C., & Wang, Y. (2008). PDL over Accelerated Labeled Transition Systems. In 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (pp. 193-200). [10.1109/TASE.2008.42] Los Alamitos: IEEE Computer Society. https://doi.org/10.1109/TASE.2008.42
    Chen, T. ; van de Pol, Jan Cornelis ; Wang, Yanjing. / PDL over Accelerated Labeled Transition Systems. 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering. Los Alamitos : IEEE Computer Society, 2008. pp. 193-200
    @inproceedings{5d9e737a955545149e841004cdfb6a67,
    title = "PDL over Accelerated Labeled Transition Systems",
    abstract = "We present a thorough study of Propositional Dynamic Logic over a variation of labeled transition systems, called accelerated labelled transition systems, which are transition systems labeled with regular expressions over action labels. We study the model checking and satisfiability decision problems. Through a notion of regular expression rewriting, we reduce these two problems to the corresponding ones of PDL in the traditional semantics (w.r.t. LTS). As for the complexity, both of problems are proved to be Expspace-complete. Moreover, the program complexity of model checking problem turns out to be Nlogspace-complete. Furthermore, we provide an axiomatization for PDL which involves Kleene Algebra as an Oracle. The soundness and completeness are shown.",
    keywords = "EWI-12952, METIS-251038, IR-64837, CR-F.3.1",
    author = "T. Chen and {van de Pol}, {Jan Cornelis} and Yanjing Wang",
    note = "10.1109/TASE.2008.42",
    year = "2008",
    month = "6",
    doi = "10.1109/TASE.2008.42",
    language = "Undefined",
    isbn = "978-0-7695-3249-3",
    publisher = "IEEE Computer Society",
    number = "302",
    pages = "193--200",
    booktitle = "2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering",
    address = "United States",

    }

    Chen, T, van de Pol, JC & Wang, Y 2008, PDL over Accelerated Labeled Transition Systems. in 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering., 10.1109/TASE.2008.42, IEEE Computer Society, Los Alamitos, pp. 193-200, 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, Nanjing, China, 17/06/08. https://doi.org/10.1109/TASE.2008.42

    PDL over Accelerated Labeled Transition Systems. / Chen, T.; van de Pol, Jan Cornelis; Wang, Yanjing.

    2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering. Los Alamitos : IEEE Computer Society, 2008. p. 193-200 10.1109/TASE.2008.42.

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - PDL over Accelerated Labeled Transition Systems

    AU - Chen, T.

    AU - van de Pol, Jan Cornelis

    AU - Wang, Yanjing

    N1 - 10.1109/TASE.2008.42

    PY - 2008/6

    Y1 - 2008/6

    N2 - We present a thorough study of Propositional Dynamic Logic over a variation of labeled transition systems, called accelerated labelled transition systems, which are transition systems labeled with regular expressions over action labels. We study the model checking and satisfiability decision problems. Through a notion of regular expression rewriting, we reduce these two problems to the corresponding ones of PDL in the traditional semantics (w.r.t. LTS). As for the complexity, both of problems are proved to be Expspace-complete. Moreover, the program complexity of model checking problem turns out to be Nlogspace-complete. Furthermore, we provide an axiomatization for PDL which involves Kleene Algebra as an Oracle. The soundness and completeness are shown.

    AB - We present a thorough study of Propositional Dynamic Logic over a variation of labeled transition systems, called accelerated labelled transition systems, which are transition systems labeled with regular expressions over action labels. We study the model checking and satisfiability decision problems. Through a notion of regular expression rewriting, we reduce these two problems to the corresponding ones of PDL in the traditional semantics (w.r.t. LTS). As for the complexity, both of problems are proved to be Expspace-complete. Moreover, the program complexity of model checking problem turns out to be Nlogspace-complete. Furthermore, we provide an axiomatization for PDL which involves Kleene Algebra as an Oracle. The soundness and completeness are shown.

    KW - EWI-12952

    KW - METIS-251038

    KW - IR-64837

    KW - CR-F.3.1

    U2 - 10.1109/TASE.2008.42

    DO - 10.1109/TASE.2008.42

    M3 - Conference contribution

    SN - 978-0-7695-3249-3

    SP - 193

    EP - 200

    BT - 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering

    PB - IEEE Computer Society

    CY - Los Alamitos

    ER -

    Chen T, van de Pol JC, Wang Y. PDL over Accelerated Labeled Transition Systems. In 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering. Los Alamitos: IEEE Computer Society. 2008. p. 193-200. 10.1109/TASE.2008.42 https://doi.org/10.1109/TASE.2008.42