Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 5, October 2002: pp. 839-859

The Expressive Power of Temporal Logic of Actions

Arkady Estrin1 and Michael Kaminski2

1diCarta Inc., 600 Allerton Street, Redwood City, CA 94063, USA. E-mail: aestrin@dicarta.com
2Department of Computer Science, Technion - Israel Institute of Technology, Haifa 32000, Israel. E-mail: kaminski@cs.technion.ac.il

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.

Keywords: Temporal interpretations; invariance under stuttering

Table of Contents   Full-Text PDF (203 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement