Abstract
Alternating Time Temporal Logic (ATL) [2] has proved useful in specifying systems that can be viewed as the parallel composition of a set of agents. It has tool-support for model checking and simulation in the form of Mocha [1]. ATL* is a more expressive form of ATL which provides a more natural way to write specifications. Whilst ATL can be model checked in linear time (relative to the size of the model), ATL* is 2EXPTIME-complete [2]. Here we present a method of “translating” an ATL* formula, into ATL so that model checking can then be performed. This method cannot, in general, be entirely exact but instead produces a strong and a weak bound. From these we may be able to infer whether the original formula was satisfied. To minimise the number of undecided cases, the bounds must be as close as possible to the original. Exact translations help to ensure that this is so, and we have identified a subset of ATL* which can be translated without loss. Case studies support the method by showing that most ATL* formulae attempted did yield conclusive results, even after approximation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, T. A. Henzinger, S. C. Krishnan, et al. Mocha User Manual. Computer and Information Science Department, University of Pennsylvania and Electrical Engineering and Computer Sciences Department, University of California, Nov. 1999.
R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science, pages 100–109. IEEE Computer Society Press, 1997.
F. Cassez, M. D. Ryan, and P.-Y. Schobbens. Proving feature non-interaction with alternating-time temporal logic. In S. Gilmore and M. D. Ryan, editors, Language Constructs for Describing Features. Springer-Verlag, 2000.
M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. In Proceedings of the 21st International Conference on Software Engineering, May 1999.
E. A. Emerson and J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences, 30(1):1–25, Feb. 1985.
L. Lamport. “Sometimes” is sometimes “not never” — on the temporal logic of programs. In Proc. 7th ACM Symposium on Principles of Programming Languages, pages 174–185, Jan. 1980.
L. Lamport. What good is temporal logic? In R. E. A. Mason, editor, Proceedings of the IFIP Congress on Information Processing, pages 657–667. North-Holland, 1983.
T. Laureys. From event based semantics to linear temporal logic. Master’s thesis, School of Cognitive Science — University of Edinburgh, 2 Buccleuch Place, Edinburgh, UK, 1999.
F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In Proceedings of 10th International Conference on Computer Aided Verification, pages 248–263. Springer-Verlag, 2000.
T. Wilke. CTL+ is exponentially more succinct than CTL. In C. P. R. et al., editor, Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 1738 of Lecture Notes in Computer Science, pages 110–121. Springer Verlag, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Harding, A., Ryan, M., Schobbens, PY. (2002). Approximating ATL* in ATL. In: Cortesi, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2002. Lecture Notes in Computer Science, vol 2294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47813-2_20
Download citation
DOI: https://doi.org/10.1007/3-540-47813-2_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43631-7
Online ISBN: 978-3-540-47813-3
eBook Packages: Springer Book Archive