Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation

By Gourinath Banda, Roskilde University, Denmark,
John P. Gallagher Roskilde University, Denmark and IMDEA Software, Madrid.

The full version of this work will appear in the Proceedings of the 16th LPAR conference, Dakar, Senegal, May 2010.

PDF Version

Introduction

In this work we apply the framework of abstract interpretation [5] to design and implement an abstraction of temporal logic. Then we apply this approach to verify temporal properties of real-time system models (expressed as CLP programs), using a domain based on linear constraints, and an implementation in CLP interfaced to the PPL library and an SMT solver.

Some previous work in temporal abstraction handles only universal formulas (e.g. [4]) or use extra conceptual apparatus in the semantics such as mixed or modal transition systems (e.g. [6, 9]) in order to approximate the meaning of arbitrary formulas. By contrast our approach is able to approximate safely the meaning of any formulas, with no restriction on the occurrence of existential and universal quantifiers.

The present work is part of an attempt to develop a uniform constraint-based
formal modelling and verification framework for verifying infinite state reactive systems. The modelling part of this framework was considered in [3, 2] where it was shown how to model linear hybrid automata (LHA) specifications as constraint logic programs.

Temporal logics and finite model checking

The use of temporal languages such as CTL, LTL and the μ-calculus for expressing properties of reactive, real-time systems has become widespread. Their semantics is based on Kripke structures, which are transition systems with a property-labelling function returning the set of propositions that are true in each state.

Given a Kripke structure K modelling some system of interest with states S, functions pre : 2^S → 2^S, : 2^S → 2^S and states : → 2^S express essential properties of the structure.

• pre(S′) = {s∣∃s^′ ∈ S^′ : (s,s^′) ∈ Δ} returns the set of states having at least one of their successors in the set S′⊆ S;
• (S′) = compl(pre(compl(S′))) returns the set of states all of whose successors are in the set S′⊆ S; the function compl(X) = S \ X.
• states(p) = {s ∈ S∣p ∈ L(s)} returns the set of states where p ∈ holds.

Using these functions, a function [[.]] is defined that evaluates the set of states where a temporal logic formula holds. The expression [[ϕ]] returns the set of states at which formula ϕ holds. Model checking consists of checking whether the Kripke structure K possesses a property ϕ, written Kϕ. This is defined to be true iff I ⊆ [[ϕ]], where I is the set of initial states, or equivalently, that I ∩ [[¬ϕ]] = ∅.

When the state-space S is infinite, the evaluation of [[.]] might not terminate and
hence the model checking of infinite state systems becomes undecidable. In this case
we try to approximate [[.]] using the theory of abstract interpretation.

Abstract interpretation and infinite state model checking

In abstract interpretation we develop an abstract semantic function systematically from the standard (“concrete”) semantics. The formal framework is based on a Galois connection (α , γ ) between the lattices ⟨L,⊑_L⟩ and ⟨M,⊑_M⟩ between the lattices ⟨L,⊑_L⟩ and ⟨M,⊑_M⟩ which are the concrete and abstract semantic domains respectively.

The functions  α  and γ are known as the abstraction and concretisation functions respectively.

For our purposes we only consider abstractions based on Galois connections (α , γ ), where the concrete domain 2^S consists of sets of concrete states and the abstract domain 2^A consists of sets of abstract states. (In fact the abstract domain could be any lattice but the presentation become somewhat more complex).

Given such a Galois connection, the concrete functions pre, , and states
defined earlier are abstracted by their best possible counterparts over the abstract
domain, yielding the following abstract functions.

We simply substitute apre, and astates for their concrete counterparts in the
concrete semantic function to obtain abstract semantics [[.]]^a for the temporal
logic. The properties of Galois connections ensure that α([[ϕ]]) ⊆ [[ϕ]]^a and
γ([[ϕ]]^a) ⊇ [[ϕ]].

The main result

As a consequence, for any Kripke structure K and ϕ a temporal formula, if γ([[¬ϕ]]^a) ∩ I = ∅ then Kϕ.

This result provides us with a sound abstract model checking procedure for any temporal logic formula ϕ. Namely, given a formula ϕ to check, we evaluate the abstract semantics of its negation, [[¬ϕ]]^a. If this represents a set of states that is disjoint from the initial states, then the property is satisfied. Of course, if γ([[¬ϕ]]^a) ∩ I ⊃∅ nothing can be concluded.

Experiments with a constraint-based abstraction

We consider transition systems derived from Linear Hybrid Automata (LHAs) whose states are n-tuples of real numbers, and abstractions of the state space based on a finite partition, which are also represented using linear constraints. In the paper it is shown how constraint representation of all the semantic functions pre, and states and the abstraction functions ? and ? are constructed. Hence the abstract functions apre, and astates can also be constructed by composing the basic functions. A CLP implementation, interfaced to powerful tools, namely the Parma Polyhedra Library (PPL) [1] and the SMT solver Yices [7], was constructed, yielding an effective abstract model checker. This was applied successfully to a number of LHAs models, proving safety, liveness and progress properties.

A critical area of future research is the selection of abstractions (such as a partition of the state space) and strategies for refining the abstraction if it turns out to be too coarse to prove the required property. Constructing the abstract semantics completely using the standard techniques of abstract interpretation provides a general framework for refinement, for example building on the techniques of Ganty [8].

References

1. R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming, 72(1–2):3–21, 2008.

Acknowledgments

Work partly supported by the Danish Natural Science Research Council project SAFT: Static Analysis Using Finite Tree Automata.