Tytuł artykułu
Autorzy
Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
Abstrakty
We show that a stutter-invariant property is expressible in propositional temporal logic without the "until" operator if and only if it is expressible in the Generalized Temporal Logic of Actions.
Wydawca
Czasopismo
Rocznik
Tom
Strony
127--140
Opis fizyczny
bibliogr. 8 poz.
Twórcy
autor
- Computer Science Department, Technion-Israel Institute of Technology, Haifa 32000. Israel, kaminski@cs.technion.ac.il
Bibliografia
- [1] Abadi, M.: An Axiomatization of Lamport's Temporal Logic of Actions, Proceedings of CONCUR'90: Theories of concurrency: unification and extension (J. Baeten, J. Klop, Eds.), Springer Verlag, Berlin, 1990, Lecture Notes in Computer Science 458.
- [2] Browne, M., Clarke, E., Grumberg, O.: Characterizing Finite Kripke Structures in Propositional Temporal Logic, Theoretical Computer Science, 59, 1988, 115-131.
- [3] Clarke, E., Grumberg, O., Peled, D.: Model Checking, MIT Press, Cambridge, MA, 1999.
- [4] Kaminski, M.: Invariance under stuttering in a temporal logic of actions, Theoretical Computer Science, 368, 2006, 50-63.
- [5] Kučera, A., Strjček, J.: The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL, Proceedings of 16th International Workshop on Computer Science Logic, CSL 2002, and the 11th Annual Conference of the EACSL (J. Bradfield, Ed.), Springer Verlag, Berlin, 1994, Lecture Notes in Computer Science 458.
- [6] Lamport, L.: The Temporal Logic of Actions, ACM Transactions on Programming Languages and Systems, 16, 1994, 872-923.
- [7] Merz, S.: A More Complete TLA, Proceedings of FM'99 - Formal Methods: World Congress on Formal Methods in the Development of Computer Systems, Volume II (J.Wing, J.Woodlock, J. Davies, Eds.), Springer Verlag, Berlin, 1999, Lecture Notes in Computer Science 1709.
- [8] Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator, Information Processing Letters, 63, 1997, 243-246.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BUS5-0014-0062