Invariance Under Stuttering in a Temporal Logic without the "Until" Operator

• Autorzy: Kaminski M.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

propositional temporal logic; temporal interpretations; invariance under stuttering

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 82, nr 1-2
• Strony: 127--140
• Opis fizyczny: bibliogr. 8 poz.

Twórcy

autor

Kaminski M.

• Computer Science Department, Technion-Israel Institute of Technology, Haifa 32000. Israel,

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.