PDL over Accelerated Labeled Transition Systems

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

doi:10.1109/TASE.2008.42

PDL over Accelerated Labeled Transition Systems

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

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

1 Citation (Scopus)

60 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 language	Undefined
Title of host publication	2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering
Place of Publication	Los Alamitos
Publisher	IEEE Computer Society
Pages	193-200
Number of pages	8
ISBN (Print)	978-0-7695-3249-3
DOIs	https://doi.org/10.1109/TASE.2008.42
Publication status	Published - Jun 2008
Event	2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008 - Nanjing, China Duration: 17 Jun 2008 → 19 Jun 2008 Conference number: 2

Publication series

Name
Publisher	IEEE Computer Society Press
Number	302

Conference

Conference	2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008
Abbreviated title	TASE
Country	China
City	Nanjing
Period	17/06/08 → 19/06/08

Keywords

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

Access to Document

10.1109/TASE.2008.42

TASE08-PDL
open
TASE08-PDL
open

Cite this

@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 ; null ; Conference date: 17-06-2008 Through 19-06-2008",

year = "2008",

month = jun,

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 proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - PDL over Accelerated Labeled Transition Systems

AU - Chen, T.

AU - van de Pol, Jan Cornelis

AU - Wang, Yanjing

N1 - Conference code: 2

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

Y2 - 17 June 2008 through 19 June 2008

ER -