Fluent model checking for event-based systems

12 years 4 days ago
Fluent model checking for event-based systems
Model checking is an automated technique for verifying that a system satisfies a set of required properties. Such properties are typically expressed as temporal logic formulas, in which atomic propositions are predicates over state variables of the system. In event-based system descriptions, states are not characterized by state variables, but rather by the behavior that originates in these states in terms of actions. In this context, it is natural for temporal formulas to be built from atomic propositions that are predicates on the occurrence of actions. The paper identifies limitations in this approach and introduces “fluent” propositions that permit formulas to naturally express properties that combine state and action. A fluent is a property of the world that holds after it is initiated by an action and ceases to hold when terminated by another action. The paper describes an approach to model checking fluent-based linear-temporal logic properties, with its implementation and a...
Dimitra Giannakopoulou, Jeff Magee
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Authors Dimitra Giannakopoulou, Jeff Magee
Comments (0)