Expressing Iterative Properties Logically in a Symbolic Setting

We present a logic for reasoning about LOTOS behaviours which allows properties involving repeated patterns over actions and data to be expressed. The semantics of the logic is given with respect to symbolic transition systems. Several motivational examples are included. The reader is assumed to have passing familiarity with LOTOS.

• Type: Conference
• Year: 2004
• Where: AMAST
• Authors: Carron Shankland, Jeremy Bryans, Lionel Morel
• Keywords: AMAST 2004, LOTOS Behaviours, Several Motivational Examples, Software Engineering, Symbolic Transition Systems