Wednesday, June 14, 2006

Linear Temporal Logic (1)

As their name suggests, temporal logics are logics where truth values of formulas may change over time. The significance of temporal logic in computer science is indisputable, especially in verification of safety-critical reactive systems. Model checkers of many flavors of temporal logics have been developed to the extent that they can quickly verify real-world systems with a huge number of states. Furthermore, in contrast to many other tools and techniques of formal methods which are semi-automatic and relatively expensive, model checking is fully-automatic and quite cheap (excellent free model checkers like SPIN exist). Last year these tools and techniques were awarded the ACM Paris Kanellakis Theory and Practice Award. Amir Pnueli, the researcher who introduced the idea of using temporal logic in verification, was awarded the ACM Turing Award in 1996.

As we mentioned, temporal logic comes in a number of flavors. At present we deal only with Linear Temporal Logic (LTL). It is linear because we evaluate each LTL formula with respect to a vertex-labeled infinite path p0p1..., where each vertex pi in the path corresponds to a point in time. "Present" is p0. "Future" is any of pi with i ≥ 0. Each vertex is labeled by a subset of 2Σ where Σ is a set of atomic propositions. In other words, the label of a vertex indicates which atomic propositions are true in that vertex. Here is a somewhat contrived example. Suppose that Σ = {a,b}. As an example, take the path {a}2000{a,b}ω, which is a path whose first 2000 vertices are {a}-labeled and the rest of the vertices are {a,b}-labeled. An example of an LTL formula is "at some point in the future, 'b' holds", which is true. Another example is "a holds until b holds", which is also true.

More formally, the syntax of LTL formulas can be defined in Backus-Naur form as follows:

φ, ψ := p (p ∈ Σ) | φ ∧ ψ | ¬ φ | X φ | φ U ψ

Given a 2Σ-labeled (infinite) path w, we write wi to refer to the infinite subpath of w starting from the ith vertex (the initial vertex is the 0th vertex). We may now define the semantics of LTL formulas:

1. w |= p (p ∈ Σ) if the label of the initial vertex of w contains p
2. w |= φ ∧ ψ if w |= φ and w |= ψ
3. w |= ¬ φ if it is not the case that w |= φ
4. w |= X φ if w1 |= φ
5. w |= φ U ψ if there exists j ≥ 0 such that wj |= ψ and for all 0 ≤ i < j, we have wi |= φ

We use F φ to abbreviate "true U φ", which says that φ holds in some future. Note that "future" also includes the present. We use G φ to abbreviate ¬ F ¬ φ, which says that φ must hold at all points in the path, i.e., globally. Finally, note that {¬,∧} captures all other boolean connectives, which allows us to freely use any boolean connectives when we write formulas.

How do we use LTL to verify real world systems? The answer requires that we first define the semantics of LTL formulas with respect to Kripke Structures. A Kripke structure K over a finite alphabet Σ is a tuple (S,E,λ: S -> 2Σ), where S is a set of vertices (or states)and E a set of directed edges on S. It is normally assumed that each vertex in S has at least one outgoing edge. The function λ defines which propositions in Σ are true in a given state. The reader should convince himself that the notion of Kripke structures can be used to model many practical systems. You can first start with traffic lights, in which case &Sigma = {green,red,yellow}, S consists of three states (each corresponding to the event where the light is green, red, or yellow), and E models how traffic lights work (e.g. green -> yellow -> red). A more interesting example includes Dijkstra's algorithm for the dining philosopher problem.

Now, given a state s in structure K, we may define the semantics of LTL formulas: K,s |= φ if for all directed path w in K starting from s, we have w |= φ. For example, if K models traffic lights, then the formulas G( green -> F red ) and G( green -> X yellow ) have to hold in every state of K. [For example, the first formula says that, it is globally true that if the light is presently green, then at some point in the future it will turn red.]

What we are interested in is an algorithm that solves the following model-checking problem: given a Kripke structure K over Σ, a state s in K, and an LTL formula φ over Σ, decide whether K,s |= φ. The problem is PSPACE-complete. The best known algorithm, which runs in 2O(|φ|) x |K|, was given by Vardi and Wolper by utilizing automata theory on infinite strings. Although the complexity of the algorithm is exponential in the size of the formula, the algorithm runs quite fast in practice because practical specifications are usually short. We shall talk about this algorithm in the near future.

Rachelle said...

Awesome!

halaman rumah said...

articles that I like

cara beli rumah tanpa modal said...

Very beautiful, this blog write very meaningful,your article is really Great

perumahan baru di tangerang said...

your articles that I like :D

harga rumah saat ini said...

thanks for knowledge master

rumah bebas banjir said...

I am very happy with this record, thanks

model rumah minimalis said...

Very beautiful, this blog write very meaningful,your article is really Great

rumah hak milik said...

I really enjoyed every article written on this blog :)

perumahan di sawangan depok said...

thank you for your sharing.it is very good. :)

green orchid residence bsd said...

thanks to sharing article master :)

rumah dijual di serpong said...

very useful information :)

Rumah Minimalis 1 Lantai Dijual said...

thanks to sharing master

Perumahan di pamulang said...

I am very happy with this record, thanks :)

Perkembangan kota Cibinong said...

article very useful for me :)

Perumahan di pamulang said...

Perumahan Trevista Ciputat said...

site Its really informative :)

perumahan griya cibinong asri said...

I strongly agree with your article :)

Membeli Rumah Bebas Banjir said...

i like your article, thanks to sharing master :)

Perkembangan Investasi Saat In said...

Very beautiful, this blog write very meaningful,your article is really Great :)

membeli properti melalui lelan said...

I am very happy with this record, thanks :)

Tips Membeli Rumah di Komplek said...

thank you. awaited next article :)

Pilihlah Gaya Rumah Idaman And said...

sometimes looking for information in accordance with the purposes it was hard :)

properti saya bravesite said...

i like your article, thanks to sharing master :)

SIFAT FISIK TAPAK YANG PENTING said...

thank you for sharing this information very useful :)