Abstract
| 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 | |
| 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
Cite this
}
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 - 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 -