Home

Counting Fluents Linear-Time Temporal Logic may be suitable to express properties of reactive systems. However, its adoption would be seriously affected by the lack of analysis mechanisms for the logic. Model checking provides an automated method for determining whether or not a property holds on the system's state graph.

In order to be able to define a model checking procedure, it is important to guarantee finiteness of the model and properties being analysed. In order to keep counting fluents bounded, we propose restricting them with bounds and scopes, two kinds of numerical limits to counting fluents.
Given the limits to the counting fluents, our approach is based on the definition of a process that monitors the occurrence of the events that update the states of the counting fluents present in the property being analysed. A monitor process activates propositional fluents that capture the truth value of the fluent expressions of the properties formulas, when relevant events occur. Finally, CFLTL formulas are encoded as FLTL formulas, by replacing the counting expressions with corresponding propositional fluents and considering states in which monitors are updating fluent values as unobservable.

Bounds and Scopes

A bound is a limit that arises as part of modelling, and comes from an actual constraint on the system being specified. For instance, suppose that we are modelling a mobile phone whose volume is restricted to be at most max. Relating this value to events, clearly once max is reached, further presses on the “increase volume” button have no effect on the volume, and therefore can be ignored (at least regarding what concerns the behaviour of the mobile phone).
A counting fluent associated with increasing the volume can then be restricted by max as its largest possible value.

Unbounded counting fluents, on the other hand, must be limited by scopes, to maintain the analysis being fully automated. As an example of an unbounded counting fluent, that will have to be limited by a scope, consider an ACK in a model of a TCP protocol. As opposed to the case of bounds, which are part of the model, scopes are necessary due to analysis reasons.

When a lower (resp. upper) bound is reached, decrementing (resp. incrementing) events are ignored, i.e., the value of the counting fluent remains the same. When a lower (resp. upper) scope is reached, analysis becomes inconclusive. That is, exceeding a scope during analysis corresponds to reaching fluent overflow states, and thus from models with reachable “overflowed” states nothing can be inferred, neither the validity of the property, nor the construction of a counterexample.

The Tool: CF-LTSA

The described approach to CFLTL model checking allows to verify properties containing counting expressions using LTSA. Labelled Transition System Analyser (LTSA) is a verification tool for concurrent systems models. A system in LTSA is modelled as a set of interacting finite state machines. LTSA supports Finite State Process notation (FSP) for concise description of component behaviour, and directly supports FLTL verification by model checking.

Counting Fluents Labelled Transition System Analyser (CF-LTSA) is a prototype extension of LTSA that allows to declare and use (by means of counting expressions on formulas) counting fluentes for system analysis.
Syntactically, counting fluents can be defined via the following syntax:

In order to use counting fluents for system analysis, properties with counting expressions (as part of a LTL formula) can be verified. The counting expressions allowed by CF-LTSA are:

where cf_expr are one of the three below options:

Once counting fluents are defined and a property specified (1), the system must be compiled (2 y 3) and composed in order to get the corresponding monitor and translated formula to FLTL (4). Then, the property can be verified (5) or the system can be simulated (6).