On-the-fly Verification for Product-LTL

Deepak D’Souza^{∗}  P. Madhusudan^{†}

1 Introduction

The propositional linear temporal logic LTL [P 77] is a well studied tool for specifying and reasoning about distributed programs. An important application of LTL is in the area of model-checking, where given a (usually finite-state) program and a specification of the program written as an LTL formula, the problem is to check if all the runs of the program are models of the formula, i.e. satisfy the specification. We will work in a setting where the program is modelled as a synchronised product of a finite number of sequential programs. In [T 95] Thiagarajan defines a temporal logic Product-PTL (or Product-LTL), which can describe boolean combinations of LTL assertions about the individual sequential components. In this paper, we propose an on-the-fly technique for model-checking such programs against Product-LTL specifications.

When concurrent or distributed programs are modelled as a finite-state transition system, there is an inherent exponential blow-up of the state-space in terms of the number of processes. This so-called “statespace explosion” problem is the main practical difficulty in verifying large programs. Much of this state-space explosion arises because the model describes all possible interleaved runs of the original program. However, it has been noticed that to check certain trace consistent properties one can equate many interleaved runs of the program, and check the property along a single representative run of each such equivalence class. This is the basis for many partial-order based verification methods ([G 96], [V 90]) which lead to marked reduction in time and space in practical model-checking.

In our setting, where we work with networks of communicating automata which co-ordinate by synchronising on common actions, there is a natural notion of independence – two actions are independent if they are performed by disjoint sets of agents. Using standard notions of Mazurkiewicz traces, this leads to an equivalence relation on global runs of the network. Now, models of Product-LTL formulas are always trace-consistent [T 95], and this is what makes it an interesting logic to study from the model-checking point of view.

For practical verification, it is desirable to have what is known as an on-the-fly model-checker. To understand this, let us consider the following automata-theoretic approach to model-check Product-LTL specifications. Given a distributed program and a Product-LTL specification φ, we do the following:

1. View the program as a product automaton, say M.

2. Build a product automaton for the negation of the specification, say A_{¬φ}, which describes all the ways in which a program might fail to meet the specification φ.

3. Construct the intersection of M and A_{¬φ}, say C.

4. Check whether the language accepted by C is empty. The language is empty if and only if the program satisfies the specification.

Now, for doing Step 4 of the above procedure, there are good algorithms (like [CVWY 92]) which do a depth-first search on C and which can report non-emptiness after looking at just some initial portion of the automaton. Hence C can be incrementally constructed as and when required by the algorithm running Step 4. If we now have a procedure for building A_{¬φ} in Step 2 in an incremental as-is-needed (or on-the-fly) manner, then we could construct C on the fly, and, in case Step 4 reports an intersection early, we can report that the program fails to meet the specification and stop. In such a case, we would save the space and time needed to construct the complete product automaton A_{¬φ}. Since for a given φ, A_{¬φ} could be exponential in |φ|, we could benefit considerably by such a method. Hence we will have an on-the-fly model-checker if we can do Step 2 on the fly.

∗SPIC Mathematical Institute, 92 G. N. Chetty Rd, Madras - 600017. email: deepak@smi.ernet.in

†Institute of Mathematical Sciences, Taramani, Madras - 600113. email: madhu@imsc.ernet.in

In [VWS 83] the authors first showed how to construct a Büchi automaton which will accept the models of a given LTL formula. In [GPVW 95], the authors give a simple on-the-fly algorithm to generate automata for LTL formulas and in [M 96] we showed how to extend this to an action-based logic LTL(Σ). In this paper, we show how we can use this algorithm to construct a product automaton for Product-LTL formulas, in an on-the-fly manner.

2 Preliminaries

For a set X, let X^{ω} denote the set of infinite sequences over X, i.e. the set of maps f : ℕ → X. Let X^{∞} denote the set (X^{∗} ∪ X^{ω}). For x ∈ X^{∞}, let pre(x) be the set of finite prefixes of x. For a string σ ∈ X^{∞}, and i ≥ 0 let σ_{i} denote the i-th suffix of σ. In case i ≥ |σ|, σ_{i} is defined to be the empty word ϵ. Similarly, for a map f : pre(σ) → Y, we define f_{i} : pre(σ_{i}) → Y given by f_{i}(τ) = f(τ′ · τ) where σ = τ′ · σ_{i}.

Definition 2.1 A Labelled Generalised Büchi Automaton (LGBA) over an alphabet Σ is a tuple (Q, ⟶, I, F, G, l) where Q is a finite set of states, ⟶ ⊆ Q × Σ × Q is the transition relation, I ⊆ Q is a set of start states, F ⊆ Q is a set of finitary final states, G ⊆ 2^{Q} is a set of sets of infinitary final states, and l is the labelling function which associates with each state a set of labels from a finite domain D; i.e. l : Q → 2^{D}.

Let A = (Q, ⟶, I, F, G, l) be an LGBA over Σ. Let σ ∈ Σ^{∞}. A run ρ of A on σ is a map ρ : pre(σ) → Q such that (i) ρ(ϵ) ∈ I, and (ii) ∀τa ∈ pre(σ) ρ(τ) ⟶^{a} ρ(τa).

For a run ρ on σ define inf (ρ) = {q ∈ Q | for infinitely many τ ∈ pre(σ), ρ(τ) = q}.

A run ρ of A on σ is accepting if either σ is finite and ρ(σ) ∈ F, or, σ is infinite and inf (ρ) ∩ G ≠ ∅, for each G ∈ G. We say that a run ρ on σ is labelled by a map ξ : pre(σ) → D if for all τ ∈ pre(σ) ξ(τ) ∈ l(ρ(τ)).

A pair (σ, ξ) is accepted by A if there exists an accepting run of A on σ labelled by ξ. We define the language accepted by A as L(A) = {(σ, ξ) | σ ∈ Σ^{∞}, ξ : pre(σ) → D, and (σ, ξ) is accepted by A}.

3 Action-based LTL

Let Σ be a finite set of action symbols and P a finite set of propositional symbols. We define an action based version of LTL called LTL(Σ) whose models are sequences of propositional valuations along with a sequence of actions.

3.1 Syntax and semantics

The formulas of LTL(Σ) are given by the following abstract syntax

ϕ ::= p (p ∈ P) | ¬ϕ | ϕ ∨ ϕ | Oϕ | ⟨a⟩ϕ | ϕUϕ .

Let φ be an LTL(Σ) formula. A model for φ is of the form (σ, ξ) where σ ∈ Σ^{∞}, and ξ : pre(σ) → 2^{P}. The satisfaction relation (σ, ξ) ⊧_{Σ} φ is defined inductively:

(σ, ξ) ⊧_{Σ} p  iff p ∈ ξ(ϵ)
(σ, ξ) ⊧_{Σ} ¬α  iff (σ, ξ) |̸=_{Σ} α
(σ, ξ) ⊧_{Σ} α ∨ β iff (σ, ξ) ⊧_{Σ} α or (σ, ξ) ⊧_{Σ} β
(σ, ξ) ⊧_{Σ} Oα iff σ ≠ ϵ and (σ_{1}, ξ_{1}) ⊧_{Σ} α
(σ, ξ) ⊧_{Σ} ⟨a⟩α iff σ = a · σ_{1} and (σ_{1}, ξ_{1}) ⊧_{Σ} α
(σ, ξ) ⊧_{Σ} αUβ iff ∃k ≥ 0 s.t. (σ_{k}, ξ_{k}) ⊧_{Σ} β and ∀i : 0 ≤ i < k, (σ_{i}, ξ_{i}) ⊧_{Σ} α.

Define L_{Σ}(φ) = {(σ, ξ) | (σ, ξ) ⊧_{Σ} φ}.

3.2 Formula automaton

In [M 96] Madhusudan gives an algorithm to build a formula automaton (an LGBA) for an LTL(Σ) formula, in an on-the-fly manner. We can think of the algorithm as comprising two procedures: init, which gives us the initial states of the automaton, and adj which gives us the set of states adjacent to a given state. States in the automaton are simply finite sets of LTL(Σ) ^{1} formulas.

adj is a non-deterministic procedure which given a state, returns a set of (action, state) pairs meant to be the adjacency list of the given state. Let us fix any function

adj : P_{fin}(LTL(Σ)) → 2^{Σ×P_{fin} (LTL(Σ))},

such that for each X ⊆_{fin} LTL(Σ) there is a run of adj(X) which returns the set adj (X). Similarly, let init be any function which given φ ∈ LTL(Σ) returns a set of states returned by some run of init . The thesis then proves the following property: Let

A_{φ} = (Q, ⟶, I, F, G, l) where

• Q is any finite subset of P_{fin}(LTL(Σ)).

• ∀p ∈ Q, p ⟶^{a} q iff (a, q) ∈ adj (p).

• I = init(φ).

• F = ∅ .

• Let {α_{1}Uβ_{1} , …, α_{r}Uβ_{r} } be the set of until formulas in CL(φ) – the subformula closure of φ. Define G = {G_{1}, …, G_{r}} where G_{i} = {q ∈ Q | β_{i} ∈ q or α_{i}Uβ_{i} ∉ q}.

• l : Q → 2^{2^{P}} given by l(q) = \{X ⊆ P | (q∩P) ⊆ X, and (\overline{X} ∩q) = ∅\}. (\overline{X} denotes the set \{¬x | x ∈ X\}.)

Then, A_{φ} accepts the set of infinite models of φ.

Further property: It is easy to adapt the algorithm for finite models, and extend the above result to say that, in addition, when

• F = {q ∈ Q | q has no formulas of the form ⟨a⟩α or Oα}, and

• G = {G_{1}, …, G_{s}} where α_{1}Uβ_{1} , …, α_{s}Uβ_{s} are the until formulas in ⋃ Q, and G_{i} = {q ∈ Q | β_{i} ∈ q or α_{i}Uβ_{i} ∉ q},

then A_{φ} accepts exactly L_{Σ}(φ).

Note that the automaton A_{φ} is completely determined by the choice of Q. Further, a property of adj is that adj(X) always returns a subset of CL(X). It follows that choosing Q to be any set containing 2^{CL(φ)} gives us a concrete realisation of A_{φ}.

We observe that A_{φ} is constructible on the fly. Essentially, this is because A_{φ} is an implicit graph, whose adjacency relation is given in terms of the adj procedure which produces the states adjacent to a given node in an incremental manner.

4 Product Automata and Product-LTL

For the rest of this paper, let us fix a distributed alphabet Σ̃ = (Σ_{1}, …, Σ_{k}). Let Σ = ⋃_{i=1}^{k} Σ_{i}. For a ∈ Σ, let loc(a) = {i | a ∈ Σ_{i}}. For σ ∈ Σ^{∞} let σ ⇂ i denote the word we get by erasing from σ all occurrences of alphabets not in Σ_{i}.

1Strictly speaking a positive form of LTL(Σ) in which negations can be driven down to the level of propositions. Dual operators ∧, V , and [a] (for ∨, U , and ⟨a⟩ respectively) are introduced for this purpose.

Definition 4.1 Let D_{1}, …, D_{k} be a partition on a finite set D. A product LGBA over Σ̃ is a structure

({A_{i}}_{i=1}^{k}, I)

where each A_{i} = (Q_{i}, ⟶_{i}, F_{i}, G_{i}, l_{i}) has the same structure as an LGBA over Σ_{i}, though without local start states. Further, the labelling function l_{i} associates with each state in Q_{i} a set of subsets of D_{i}; i.e. l_{i} : Q_{i} → 2^{2^{D_{i}}}. I ⊆ Q_{1} × ⋯ × Q_{k} is a set of global start states.

Let A = ({A_{i}}_{i=1}^{k}, I) be a product LGBA. Let A_{i} = (Q_{i}, ⟶_{i}, F_{i}, G_{i}, l_{i}). The language accepted by A is defined via a global transition relation defined as follows. Let Q = Q_{1} × ⋯ × Q_{k}. ⟶⊆ Q × Σ × Q is

given by (p_{1}, ⋯, p_{k}) ⟶^{a} (q_{1}, ⋯, q_{k}) iff ∀i ∈ loc(a), p_{i} ⟶_{i}^{a} q_{i} and ∀i ∉ loc(a), p_{i} = q_{i}.

Let σ ∈ Σ^{∞}. We say a map ρ : pre(σ) → Q is a run of A on σ if (i) ρ(ϵ) ∈ I, and (ii) for all

τ · a ∈ pre(σ), ρ(τ) ⟶^{a} ρ(τ · a).

Let ρ be a run of A on σ. We define ρ ⇂ i as a map ρ′ : pre(σ ⇂ i) → Q_{i} given by ρ′(τ) = ρ(τ′)[i], where τ′ ∈ pre(σ) such that τ = τ′ ⇂ i. Note that ρ′ is well-defined due to the fact that ρ(τ′)[i] = ρ(τ′′)[i] for all τ′, τ′′ ∈ pre(σ) such that τ′ ⇂i = τ′′ ⇂i.

A run ρ of A on σ is accepting provided for each i, ρ⇂i meets the acceptance condition of A_{i}; i.e. if σ ⇂i is finite then (ρ⇂i)(σ ⇂i) ∈ F_{i}, and if σ ⇂i is infinite, then inf (ρ⇂i) ∩ G ≠ ∅, ∀G ∈ G_{i}.

We say that a run ρ of A on σ is labelled by a map ξ : pre(σ) → 2^{D}, if ∃ξ^{1}, …, ξ^{k} such that each ξ^{i} is a labelling of the run ρ⇂i of A_{i} on σ ⇂i, and for each i ξ(τ) ∩ D_{i} = ξ^{i}(τ ⇂i).

We say that (σ, ξ) is accepted by A if there exists an accepting run of A on σ labelled by ξ. The language accepted by A is defined as L(A) = {(σ, x) | (σ, x) is accepted by A}.

Lemma 4.1 Let A_{1}, A_{2} be product LGBA’s such that A_{1} = ({A_{i}}_{i=1}^{k}, I_{1}), A_{2} = ({A_{i}}_{i=1}^{k}, I_{2}). Then L(A_{3}) = L(A_{1}) ∪ L(A_{2}) where A_{3} = ({A_{i}}_{i=1}^{k}, I_{1} ∪ I_{2}).

Definition 4.2 For languages L_{1}, …, L_{k} such that for each i L_{i} ⊆ Σ_{i}^{∞}, define

L_{1} ⊗ ⋯ ⊗ L_{k} = {σ ∈ Σ^{∞} | ∀i σ ⇂i ∈ L_{i}}.

Lemma 4.2 Let A_{i} = (Q_{i}, I_{i}, ⟶_{i}, F_{i}, G_{i}, l_{i}) (i = 1, …, k) be LGBA’s over Σ_{i}’s respectively. Then the product LGBA A = ({A_{i}}_{i=1}^{k}, I_{1} × ⋯ × I_{k}) accepts the language L(A_{1}) ⊗ ⋯ ⊗ L(A_{k}).

4.1 Product-LTL: Syntax and semantics

Fix a set of propositions P, and a partition P_{1}, …, P_{k} of P. We use the following syntax for product-LTL (denoted LTL^{⊗}:)

ϕ ::= ψ_{i} (ψ_{i} ∈ LTL(Σ_{i})) | ϕ ∨ ϕ | ϕ ∧ ϕ,

where the set of propositional symbols for LTL(Σ_{i}) is taken to be P_{i}.

The models for LTL^{⊗} formulas are pairs of the form (σ, ξ) where σ ∈ Σ^{∞}, ξ : pre(σ) → 2^{P}, satisfying the following “validity” condition: τ · a ∈ pre(σ) and a ∉ Σ_{i} ⇒ ξ(τ · a) ∩ P_{i} = ξ(τ) ∩ P_{i}.

Given a “valid” model (σ, ξ), let (σ, ξ) ⇂ i denote the pair (σ ⇂ i, ξ′) where ξ′ : pre(σ ⇂ i) → 2^{P} given by ξ′(τ) = ξ(τ′), where τ′ ∈ pre(σ) s.t. τ′ ⇂ i = τ. Note that ξ′ is well-defined due to the validity condition on (σ, ξ).

The satisfaction relation (σ, ξ) ⊧_{⊗} φ for LTL^{⊗} formulas is defined inductively as follows:

(σ, ξ) ⊧_{⊗} ψ_{i} (for ψ_{i} ∈ LTL(Σ_{i})) iff (σ, ξ)⇂i ⊧_{Σ_{i}} ψ_{i}
(σ, ξ) ⊧_{⊗} α ∨ β  iff (σ, ξ) ⊧_{⊗} α or (σ, ξ) ⊧_{⊗} β
(σ, ξ) ⊧_{⊗} α ∧ β  iff (σ, ξ) ⊧_{⊗} α and (σ, ξ) ⊧_{⊗} β

For φ ∈ LTL^{⊗} define L_{⊗}(φ) = {(σ, ξ) | (σ, ξ) ⊧_{⊗} φ}.

Note that the given syntax for LTL^{⊗} does allow us to express formulas of the form ¬α since negations can be driven in. For example, the formula ¬(p ∧ q) is equivalent to the LTL^{⊗} formula ¬p ∨ ¬q.

Lemma 4.3 Let α_{1}, …, α_{k} be formulas in LTL(Σ_{1}), …, LTL(Σ_{k}) respectively. Then L_{⊗}(α_{1} ∧ ⋯ ∧ α_{k}) = L_{Σ_{1}}(α_{1}) ⊗ ⋯ ⊗ L_{Σ_{k}}(α_{k}).

4.2 Formula automaton

Given φ ∈ LTL^{⊗} we would like to define a product automaton A_{φ} such that L(A_{φ}) = L_{⊗}(φ). We proceed in the following steps:

1. Write φ in the form α ≡ ⋁_{j=1}^{m}(⋀_{i=1}^{k} α_{i}^{j}), where ∀j, α_{i}^{j} ∈ LTL(Σ_{i}). It follows that L_{⊗}(φ) = ⋃_{j=1}^{m} L_{⊗}(⋀_{i=1}^{k} α_{i}^{j}).

2. We give A_{1}, …, A_{k}, and I^{1}, …, I^{m} such that for each j ∈ {1, …, m} the product-LGBA A^{j} = ({A_{i}}_{i=1}^{k}, I^{j}) accepts L_{⊗}(⋀_{i=1}^{k} α_{i}^{j}). This can be done by taking the formula automaton A_{α_{i}^{j}} for α_{i}^{j},

as defined in section 3, with the set of states Q taken to be ⋃_{j=1}^{m} 2^{CL(α_{i}^{j})}. Clearly, for a fixed i, this automaton is the same for each α_{i}^{1}, …, α_{i}^{m}, except for the set of initial states I_{j}^{i}. Let us write these automata as A_{α_{i}^{j}} = (A_{i}, I_{i}^{j}). Let I^{j} = I_{1}^{j} × ⋯ × I_{k}^{j}. It now follows using lemmas 4.2 and 4.3 that

A^{j} = ({A_{i}}_{i=1}^{k}, I^{j}) accepts L_{⊗}(⋀_{i=1}^{k} α_{i}^{j}).

3. From lemma 4.1 it follows that the product automaton A_{φ} = ({A_{j}}_{j=1}^{k}, ⋃_{i=1}^{m} I^{i}) accepts L_{⊗}(φ).

Thus A_{φ} is given to us implicitly in terms of the procedures init and adj for LTL(Σ_{i}). Each global initial state is an element of I_{1}^{j} × ⋯ × I_{k}^{j} (for some j ∈ {1, …, k}) where each I_{i}^{j} is the set of states returned by any single run of init(α_{i}^{j}). Similarly, to obtain the set of states adjacent to a given state q in the component automaton A_{i}, we can take the set returned by any run of adj(q) to be the set of states adjacent to q.

Acknowledgement We thank P. S. Thiagarajan for several useful discussions.

References

[CVWY 92] C. Courcoubetis, M. Vardi, P. Wolper, M. Yanakakis, Memory efficient algorithms for the verification of temporal logic properties. Formal Methods in System Design, 1992, 1, 275- 288.

[GPVW 95] R. Gerth, D. Peled, M. Vardi, P. Wolper. Simple on-the-fly verification for Linear Temporal Logic. Proc. 15th IFIP WG 6.1 Int. Workshop on Protocol Specification, Testing, and Verification. North-Holland Publ., 1995.

[G 96] Patrice Godefroid, Partial-Order Methods for the Verification of Concurrent Systems. LNCS 1032, Springer, 1996.

[M 96] P. Madhusudan. An On-the-fly Algorithm for Linear Time Temporal Logic, M. Sc. thesis, Anna University, 1996.

[P 77] A. Pnueli. The temporal logic of programs. Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46-57, 1977.

[T 95] P. S. Thiagarajan, A Trace Consistent Subset of PTL in LNCS 962, CONCUR ’95: Concurrency Theory. Insup Lee, Scott A Smolka (Eds.), 6th International Conference, Philadelphia, USA.

[V 90] Antti Valmari, Stubborn sets for Reduced State space generation. LNCS 483, 1990, pages 491-515.

[VWS 83] M. Y. Vardi, P. Wolper, A. P. Sistla. Reasoning about infinite computation paths. Proceedings of 24th IEEE Symposium on Foundation of Computer Science, Tuscan, 1983, pages 185-194.