Logic Based Abstractions of Real-Time Systems.
When verifying concurrent systems described by transition systems, state explosion is one of the most serious problems. If quantitative temporal information (expressed by clock ticks) is considered, state explosion is even more serious. We present a notion of abstraction of transition systems, where the abstraction is driven by the formulae of a quantitative temporal logic, called qu-mu-calculus, defined in the paper. The abstraction is based on a notion of bisimulation equivalence, called , n-equivalence, where  is a set of actions and n is a natural number. It is proved that two transition systems are , n-equivalent iff they give the same truth value to all qu-mu-calculus formulae such that the actions occurring in the modal operators are contained in , and with time constraints whose values are less than or equal to n. We present a non-standard (abstract) semantics for a timed process algebra able to produce reduced transition systems for checking formulae. The abstract semantics, parametric with respect to a set  of actions and a natural number n, produces a reduced transition system , n-equivalent to the standard one. A transformational method is also defined, by means of which it is possible to syntactically transform a program into a smaller one, still preserving , n-equivalence.
Introduction
In this paper we address the problem of verifying systems in which time plays
a fundamental role for a correct behaviour. We refer to the Algebra of Timed
Processes (ATP) [22] as a formalism able both to model time dependent systems
and to prove their properties. ATP is an extension of traditional process algebras
which can capture discrete quantitative timing aspects with respect to a global
clock.
We express the semantics of this language in terms of labeled transition systems
where some transitions are labeled by the special action , called time action.
Such an action represents the progress of time and can be viewed as a clock tick.
One widely used method for verication of properties is model checking [8, 7,
Model checking is a technique that proves the correctness of a system
specication with respect to a desired behavior by checking whether a structure,
representing the specication, satises a temporal logic formula describing the
expected behavior. Most existing verication techniques, and in particular those
dened for concurrent calculi, like CCS [21], are based on a representation of
the system by means of a labeled transition system. In this case, model checking
consists in checking whether a labeled transition system is a model for a formula.
When representing systems specications by transition systems, state explosion
is one of the most serious problems: often we have to deal with transition systems
with an extremely large number of states, thus making model checking
inapplicable. Moreover, when in system specications quantitative temporal information
(expressed by clock ticks) is considered, state explosion is even more
serious, the reason for this being that a new state is generated for every clock
tick. Fortunately, in several cases, to check the validity of a property, it is not
necessary to consider the whole transition system, but only an abstraction of it
that maintains the information which \in
uences" the property. This consideration
has been used in the denition of abstraction criteria for reducing transition
systems in order to prove properties e-ciently. Abstraction criteria of this kind
are often based on equivalence relations dened on transition systems: minimizations
with respect to dierent notions of equivalence are in fact used in many
existing verication environments (see, for instance, [10, 13, 16]).
In this paper we present a notion of abstraction of transition systems, where
the abstraction is driven by the formulae of a quantitative temporal logic. This
logic, which we call qu-mu-calculus, is similar to the mu-calculus [19], in particular
to a variant of it [4], in which the modal operators are redened to include
the denition of time constraints. Many logics have been dened to deal with
time aspects, see, for example [1{3, 14, 15, 20]. A fundamental feature of qu-mu-
calculus is that its formulae can be used to drive the abstraction: in particular,
given the actions and the time constraints occurring in the modal operators of a
formula  of the qu-mu-calculus, we use them in dening an abstract (reduced)
transition system on which the truth value of  is equivalent to its value on the
standard one. The abstraction is based on a notion of bisimulation equivalence
between transition systems, called h; ni-equivalence, where  is a set of actions
(dierent from the time action ) and n is a natural number: informally, two
transition systems are h; ni-equivalent i, by observing only the actions in
and the paths composed of time actions shorter than or equal to n, they exhibit
the same behaviour. Some interesting properties of such an equivalence are
presented.
We prove that two transition systems are h; ni-equivalent if and only if they
give the same truth value to all formulae such that the actions occurring in
the modal operators are contained in , and with time constraints whose values
are less than or equal to n. Thus, given a formula , with actions in  and
maximum time constraint n, we can abstract the transition system to a smaller
one (possibly the minimum) h; ni-equivalent to it, on which  can be checked.
In the paper we present a non-standard (abstract) semantics for the ASTP [22]
language, dening abstract transition systems. ASTP is the sequential subset of
ATP; actually, this is not a limitation: our abstract semantics is easily applicable
to the concurrent operators and its ability in reducing the transition system can
be suitably investigated also on the concurrent part. The abstract semantics
can be usefully exploited as a guide in implementing an algorithm to build the
reduced system.
We also present a set of syntactic rewriting rules which can transform a process
into a smaller one, while preserving h; ni-equivalence. This syntactic reduction
can be used as a rst step of the reduction process, before applying the abstract
semantics.
After the preliminaries of Section 2, we introduce our logic in Section 3 and the
abstract semantics in Section 4. Section 5 describe the syntactic transformations
and Section 6 concludes the paper.
Preliminaries
2.1 The Algebra of Timed Processes
Let us now quickly recall the main concepts about the Algebra of Timed Processes
[22], which is used in the specication of real-time concurrent and distributed
systems.
For simplicity, we consider here only the subset of ATP, called ASTP (Algebra
of Sequential Timed Processes), not containing parallel operators.
The syntax of sequential process terms (processes or terms for short) is the following

where  ranges over a nite set of asynchronous actions A :::g. We
denote by A the set A  [ fg, ranged over by :. The action  (time
action) is not user-denable and represents the progress of time. x ranges over a
set of constant names: each constant x is dened by a constant denition x def
We denote the set of process terms by P .
The standard operational semantics [22] is given by a relation !  P AP ,
where P is the set of all processes: ! is the least relation dened by the rules
in

Table

1.
Rule Act manages the prexing operator: p evolves to p by a transition labeled
by . The operator  behaves as a standard nondeterministic choice for processes
with asynchronous initial actions (rule Sum 1 and the symmetric one which is
not shown). Moreover, if p and q can perform a  action reaching respectively
can perform a  action, reaching p 0  q 0 (rule Sum 2 ).
The process bpc(q) can perform the same asynchronous initial actions as p (rule
Delay 1 ). Moreover bpc(q) can perform a  action, reaching the process q (rule
Delay 2 ). Finally, rule Con says that a constant x behaves as p if x
denition. Note that there is no rule for the process 0, which thus cannot perform
any move.
In the following we use :p to denote the term b0c(p); this process can perform
only the action  and then becomes the process p. Moreover we dene  n :p
(n > 1) as:
Act
Delay 1
Con

Table

1. Standard operational semantics of ASTP
A labeled transition system (or transition system for short) is a quadruple
is a set of states, A is a set of transition labels (actions),
is the initial state, and ! T  S  A  S is the transition relation. If
Given a process p, we write p
exist such that
is the empty sequence. Given p 2 S, we denote the
set of the states reachable from p by ! T with R !T
A  g.
Given a process p and a set of constant denitions, the standard transition system
for p is dened as p). Note that, with abuse of nota-
tion, we use ! for denoting both the operational semantics and the transition
relation among the states of the transition system.
On ASTP processes equivalence relations can be dened [22], based on the notion
of bisimulation between states of the related transition systems.
Example 1. Let us consider a vending machine with a time-dependent behavior.
The machine allows a user to obtain dierent services: a soft drink immediately
after the request; a coee after a delay of a time unit; a cappuccino after a delay
of two time units; a cappuccino with chocolate after a delay of three time units.
Moreover, it is possible to recollect the inserted coin, only if requested within
one time unit. The ASTP specication of the machine is:
V=coin brecollect money V c( coee :(collect coee V )
choc cappuccino  3 :(collect choc cappuccino V )
soft drink collect soft drink V )
The standard transition system for the vending machine has 14 states and
transitions.
3 Quantitative temporal logic and abstractions
In order to perform quantitative temporal reasoning, we dene a logic, that
we call qu-mu-calculus, which is an extension of the mu-calculus [19] and in
particular of the selective mu-calculus [4]. The syntax is the following, where Z
ranges over a set of variables:
hi R;n  j Z: j Z:
where
{ R  A  ;
{ n 2 N , where N is the set of natural numbers; n is called time value. In
hi R;<n  and [] R;<n  it must be n > 0.
The satisfaction of a formula  by a state p of a transition system, written p
is dened as follows: any state satises tt and no state satises ff; a state sat-
are the quantitative modal oper-
ators. The informal meaning of the operators is the following:
hi R;<n  is satised by a state which can evolve to a state satisfying  by
executing , not preceded by actions in R [ fg, within n time units.
[] R;<n  is satised by a state which, for any execution of  occurring
within units and not preceded by actions in R [ fg, evolves to a
state satisfying .
hi R;n  is satised by a state which can evolve to a state satisfying  by
executing , not preceded by actions in R[ fg, after at least n time units.
[] R;n  is satised by a state which, for any execution of  occurring after
at least n time units and not preceded by actions in R [ fg, evolves to a
state satisfying .
As in standard mu-calculus, a xed point formula has the form Z: (Z:)
where Z (Z) binds free occurrences of Z in . An occurrence of Z is free if it
is not within the scope of a binder Z (Z). A formula is closed if it contains no
variables. Z: is the least x point of the recursive equation
Z: is the greatest one. We consider only closed formulae.
The precise denition of the satisfaction of a closed formula  by a state p of a
transition system T is given in Table 2. It uses the relation =) ;n
Denition 1 (=) ;n
relation). Given a transition system
a set of actions   A  , and n 2 N , we dene the relation =) ;n
such that, for each  2
is the number of  actions occurring in -.
By
T q we express the fact that it is possible to pass from p to q by executing
a (possibly empty) sequence of actions not belonging to  and containing
exactly k , followed by the action  in .
A transition system T satises a formula  i its initial state satises . An
ASTP process p satises a formula  i S(p) satises .
Example 2. Examples of properties concerning the vending machine described
in the previous section are the following:
\it alway holds that, after a coin has been inserted, a soft drink may be collected
within two time units".
\ it is not possible to recollect the inserted coin after more than one time unit".
3.1 Formula driven equivalence
A formula  of the qu-mu-calculus can be used to dene a bisimulation equivalence
between transition systems. The bisimulation is dened by considering
only the asynchronous actions occurring in the quantitative operators belonging
where, for each m, Z are dened as:
where the notation [ =Z] indicates the substitution of for every free occurrence
of the variable Z in .

Table

2. Satisfaction of a formula by a state
to the formula, and the maximum time value of the quantitative operators occurring
in the formula. Thus all formulae with the same set of occurring actions
and the same maximum time value dene the same bisimulation.
Given a set   A  of actions and a time value n, a h; ni-bisimulation relates
states p and q if: i) for each path starting from p, containing k < n time actions
and no action in  and ending with  2 , there is a path starting from q,
containing exactly k time actions and no action in  and ending with  2 ,
such that the reached states are bisimilar, and ii) for each path starting from p,
containing k  n time actions and no action in  and ending with  2 , there
is a path starting from q, containing m  n (possibly m 6= actions and
no action in  and ending with  2 , such that the reached states are bisimilar.
Denition 2 (h; ni-bisimulation, h; ni-equivalence).
A  and n 2 N .
B, is a binary relation on S T  S such that rBq
implies:
- T and  are h; ni-equivalent ( T  ;n ) i there exists a h; ni-bisimulation
containing the pair (p; p 0 ).
Fig. 1. Examples of h; ni-equivalence
Example 3. Consider the transition systems illustrated in Figure 1. T1 is hfag; ni-
equivalent to T 2, with while T1 is not hfag; ni-equivalent to T 2, with
n  3. Moreover T1 is not hfa; bg; ni-equivalent to T 2, for every n 2 N .
The following proposition holds, relating equivalences with dierent  and n.
Proposition 1. For each
Proof. See Appendix A.
In order to relate h; ni-equivalence with quantitative temporal properties, we
introduce the following denition, concerning equivalences based on sets of formulae

Denition 3 (logic-based equivalence). Let T and  be two transition sys-
tems, and a set of closed formulae. The logic-based equivalence  is dened
by:
Given a formula  of the qu-mu-calculus, we dene the set of occurring actions
in  and the maximum time value of .
Denition 4. (O(), max()). Given a formula  of the qu-mu-calculus, the
set O() of the actions occurring in  is inductively dened as follows:
The maximum time value of the modal operators occurring in  (max()) is
inductively dened as follows:
The following theorem states that h; ni-equivalent transition systems satisfy the
same set of formulae with occurring actions in  and maximum time value less
than or equal to n.
Theorem 1. Let
systems and let   A  and n 2 N .
where
closed formula of the qu-mu-calculus such that O()
and max()  ng:
Proof. See Appendix A.
4 Abstract transition systems and abstract semantics
In this section, in order to reduce the number of states of a transition system
for model checking, we dene an abstraction of the transition system on which a
formula  can be equivalently checked. First we dene the notion of time path.
time path is an acyclic path composed only of  actions and such that each
state (but the rst one) has only one input transition and each state (but the
last one) has only one output transition.
Denition 5. (time path) Let transition system and
path each path p 1
that
{ holds that p i
{ 8i, 1  i < n,
6
{ 8i, 1 < i  n,
6 9q 6= p i such that q
Given an ASTP process p and a pair h; ni, we dene an abstract transition
system for p by means of a non-standard semantics which consists of a set of
inference rules that skip actions not in  and produce time paths not longer than
n. The abstract transition system is h; ni-equivalent to the standard transition
system of p.
The non standard rules are shown in Table 3 (the symmetric rules of Sum 1 and
Sum 2 are not shown). They use a transition relation ! m
;n parameterized by
an integer m  n. The ideas on which the semantics is based are the following:
{ the actions in  are always performed (rules Act 1 , Delay 4 and Sum 1 )
{ the actions not in  are skipped: when an action not in  is encountered, a
\look-ahead" is performed in order to reach either an action in  or a time
action (rules Act 2 , Delay 3 and Sum 2 );
{ when a time action is encountered, it is skipped only if the process we reach
by this action can perform a sequence of n time units. In order to count the
time units we use the superscript of ! m
;n q occurs
when an action belonging to  can be executed after m time actions starting
from p. In fact, in order to generate the transition p
;n q , we rst prove
that q
;n q 0 for some q 0 (rules Delay 1 and Delay 2 , Sum 3 and Sum 4 ).
Successive applications of Delay 2 and Sum 4 allow us to skip all time actions
in a sequence but the last n ones.
Note that in the premises of rules Delay 3 , Delay 4 , Sum 1 , Sum 2 Sum 3 and
Sum 4 the standard operational relation ! is used, in order to know the rst
action of the process and consequently to respect the standard behavior of the
operators, which is dierent depending on whether the rst action is a time
action or not.
The following proposition characterizes the transitions of the non-standard semantics

Proposition 2. Let   A  and n 2 N . For each ASTP process p,
1. p
;n q implies  2  and
2. p
Proof. By induction on depth of inference.
The proposition states that there are two kinds of transitions: the rst one
represents the execution of action  2  and is characterized by the superscript
0; the second one represents the execution of a  action, and is characterized by
a
The following result holds, relating the paths composed of time actions of the
standard transition system with those of the non-standard one:
Proposition 3. Let   A  and n 2 N . For each ASTP process p,
1. j  n and p
2. j  n and p
;n q.
Proof. See Appendix A.
The proposition states that, whenever there is a path in the standard semantics
composed of less than or equal to n time actions, followed by an action in , a
path with the same number of time actions occurs in the abstract system, while
every path with more than n time actions in the standard system corresponds
to a path with exactly n time actions in the abstract system.
Now we formally dene the notion of abstract transition system.
Denition 6 (abstract transition system). For each ASTP process p, given
A  and n 2 N the abstract transition system for p is dened as
where q
only if 9j:q
The following theorem holds, stating that the transition system dened by the
non-standard semantics is a suitable abstraction of the standard one.
Theorem 2. Let   A  and n 2 N . For each ASTP process p,
1. the transitions of N ;n (p) are labeled only either by actions in  or by ;
2. the length of each time path in N ;n (p) is less than or equal to n;
3. S(p)  ;n N ;n (p).
Proof. See Appendix A.
Note that, if the abstract transition system N ;0 (p) for a process p does
not contain transitions labeled by time actions and expresses only the precedence
properties between the asynchronous actions in . The following proposition
relates h; ni-equivalences with dierent  and n. It says that h; ni-equivalence
is preserved by keeping a larger  and a greater n.
Proposition 4. Let ;  0  A  . For
each ASTP process p,
Proof. By Proposition 1 and by Theorem 2, point 3.
Delay 1
Delay 3
;n r
;n r
;n r
Con

Table

3. Non-standard operational semantics for ASTP
Example 4. Recall the vending machine of Example 1. Let us suppose that we
have to verify the following two formulae, expressed in Example 2.
The formula 1 can be checked on the abstract transition system N 1 ;n1 (V ),
with
collect soft drinkg; and
2.
states and 14 transitions.
On the other hand 2 can be checked on N 2 ;n2 (V ), with
states and 13 transitions.
5 Syntactic reduction
In this section we investigate a syntactic approach to the reduction of transition
systems, still based on the formula to be checked. Given a process p and a
property , it is possible to perform syntactic transformations which reduce
the size of p (in terms of number of operators), based on the actions and the
time values occurring in . The transformations are h; ni-equivalence preserving,
that is  can be equivalently checked on the transformed process. The syntactic
reduction can be used independently from the semantic abstraction dened in
the previous section.

Table

4. Transformation rules
The h; ni-equivalence preserving transformations are shown in Table 4 in the
form of rewriting rules: p 7!  q means \rewrite p as q". Rule R 1 allows deleting
an asynchronous action not in , while rules R 2 and R 3 cancel time actions
from sequences of time actions. R 2 deletes m n time actions from a
sequence of m ones (if m > n), it can only be applied if the sequence is not
the operand of a summation, and this is ensured by imposing that the sequence
is prexed by an asynchronous action. When handling summations, R 3 is ap-
plied, which deletes n time actions from both operands. Note that, in order to
preserve h; ni-equivalence, in all cases the transformed term must be guarded
by an asynchronous action. The following theorem states the correctness of the
transformations.
Theorem 3. Let   A  ; n 2 N and q be an ASTP process. If q i
Proof. See Appendix A.
Other rules could be dened, performing further reductions. However, every
syntactic method, being static, cannot perform all possible simplications, since
it cannot \know" the behavior of the process at \run time". A semantic approach,
like that described in the preceding section, based on an abstract semantics, can
be in general more precise. On the other hand, compared with the semantic
approach, the syntactic one has the advantage of being less complex in time,
since it only analyzes the source code, without executing the program.
Though the semantic and syntactic reductions are independent, they can be
protably combined. Given a process p, rst it can be syntactically transformed
into a process q, and then an abstract transition system can be built for q using
the abstract semantics.
Example 5. Recall the vending machine in Example 1. Let us suppose that we
have to verify the property 2 of Example 2.
If we apply the transformation rules to the vending machine, with
fcoin; moneyg and n we obtain the following reduced process:
cappuccino :(collect cappuccino V 2)
choc cappuccino :(collect choc cappuccinoV 2)
The formula 2 can be checked on the standard transition for V 2, which has
states and 14 transitions. Moreover, 2 can be checked on the abstract
transition system N 2 ;n2 (V 2), obtained applying to V 2 the abstract semantics.
states and 9 transitions. Note that applying rst the syntactic
reduction and after the abstract semantics produces a transition system smaller
than the one obtained with the abstract semantics applied to the initial process
6 Conclusions
In this paper we have presented an approach to the problem of the reduction
of the number of states of a transition system. Many abstraction criteria for
system specications not including time constraints have been dened, see for
example [4, 6, 9, 11, 12]. For real-time systems the work [17] denes abstractions
for transition systems with quantitative labels, but there, the abstraction is not
driven by the property to be proved.
We have introduced an abstract semantics for ASTP processes in order to formally
dene the abstract transition system. Our abstract semantics is easily
applicable to the concurrent operator: Appendix B shows the extension of the
semantics to cope with this operator.
The abstract semantics can be used to design a tool for automatically building an
abstract transition system. In the implementation, some care must be taken to
manage innite loops which can occur in the look-ahead process. The syntactic
reductions are easily implementable.
The degree of reduction performed by the abstract semantics depends on the
size of the set  of actions and on the bound n. In particular, the reduction can
be signicant either when the set  is a small subset of A or when the bound n
is small with respect to the length of the time paths in the standard transition
system. Obviously, no reduction is performed if and n is greater than the
longest time path in the standard transition system.



--R

Model Checking via Reachability Testing for Timed Automata.
Logics and Models of Real Time: A Survey.
A Really Temporal Logic.
Selective mu-calculus: New Modal Operators for Proving Properties on Reduced Transition Systems
Selective mu-calculus and Formula-Based Equivalence of Transition Systems
Property Preserving Simu- lations

Automatic Veri
Model Checking and Abstraction.
The NCSU Concurrency Workbench.
Generation of Reduced Models for Checking Fragments of CTL.
Abstract Interpretation of Reactive Systems.
Aboard AUTO.


CADP A Protocol Validation and Veri
Concept of Quanti
Symbolic Model Checking for real-time Systems
Results on the propositional mu-calculus
From Timed Automata to Logic - and Back

The Algebra of Timed Processes
Local Model Checking for Real-Time Systems
--TR
Automatic verification of finite-state concurrent systems using temporal logic specifications
Communication and concurrency
Verifying temporal properties of processes
A really temporal logic
Symbolic model checking for real-time systems
The algebra of timed processes, ATP
Abstract interpretation of reactive systems
Selective mu-calculus and formula-based equivalence of transition systems
From Timed Automata to Logic - and Back
Concept of Quantified Abstract Quotient Automaton and its Advantage
Model Checking via Reachability Testing for Timed Automata
Generalized Quantitative Temporal Reasoning
Property Preserving Simulations
Generation of Reduced Models for Checking Fragments of CTL
Local Model Checking for Real-Time Systems (Extended Abstract)
Validation and Verification Toolbox
The NCSU Concurrency Workbench
Logics and Models of Real Time
Real-Time and the Mu-Calculus (Preliminary Report)
Selective MYAMPERSANDmicro;-calculus
temporal logic;ATP;state explosion