Title: The Expressive Power of Temporal Logic of Actions
Abstract: It is shown that a stutter‐invariant property is expressible in Temporal Logic of Actions if and only if it is expressible in Second‐order Temporal Logic. In particular, validity questions can be translated from one logic to the other. The proof is based on equivalence transformations between the formulas of Temporal Logic of Actions and Second‐order Temporal Logic. The translation from Second‐order Temporal Logic into Temporal Logic of Actions is linear and the translation from Temporal Logic of Actions into Second‐order Temporal Logic is quadratic.
Publication Year: 2002
Publication Date: 2002-10-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 3
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot