Talk:Kripke structure (model checking)

Hi I want to Know about how to show one concurrent model with krioke structure

---

The sentence "The labeling function L defines for each state s ∈ S the set L(s) of atomic propositions that are valid in s." is ambiguous: if L(s1) = {p2, p3}, does it meen that p1 has to be false in s1? Or CAN it be false but also true (i.e. it is not constrained)?

Proposals:

• "The labeling function L defines for each state s ∈ S the complete set L(s) of atomic propositions ..."
• "The labeling function L defines for each state s ∈ S the set L(s) of all atomic propositions ..."

--Rootworker 07:38, 17 January 2007 (UTC)

---

There should also be mentioned the terms "Timed Kripke Structure" (TKS, or "Simply-timed Kripke Structures", also called unit-delay structures (UDSs), Kripke Structures with durations on transitions) and "Symbolic Kripke Structure".

--Rootworker 07:38, 17 January 2007 (UTC)

I have found the following definition in [Extending Synchronous Languages for Generating Abstract Real-Time Models, Logothetis, Schneider]:

A Timed Kripke Structure (TKS) over a finite set of variables V is a tuple (I,S,R,L), such that

• S is a finite set of states
• I subset of S is the set of initial states
• R subset of S x N x S is a finite set of transitions

The natural number in an element in R represents the duration of a transition (action). But there exists also other definitions, like labeling a transition with an interval, or having different clocks. It would be nice having an overview of the different types...

--Rootworker 07:59, 17 January 2007 (UTC)

• • Description of the TKS in this or some other related article can also segue into timed automata and model checkers like Uppaal and Oris that avail themselves of this structure. Likewise, for this article, we could list the model checkers that avail themselves of the Kripke structure, most notably SPIN and LTSA. Vonkje (talk) 02:57, 25 November 2007 (UTC)

Kripke structures are more general than this

The literature on Kripke structures is far broader than implied here. This treatment seems to be from the perspective of finite model checking, which imposes restrictions on Kripke structures that are irrelevant to other applications while omitting much else about Kripke structures that can be found in the philosophical logic literature. (Kripke himself was a philosopher who had no idea his formalism would one day be relevant to computer science.)

If we go by Kripke's original paper, a Kripke structure is simply a pair (W, R) where W (Kripke himself (self-referentially?) wrote K) is a set of possible worlds and R is a binary relation on W. (Kripke included a "base state" G but this unnecessarily complicates the concept.)

A Kripke model over a set Σ₀ of propositional variables or atoms is a Kripke structure together with a truth value assignment φ: Σ₀×W → 2 giving the truth value of each propositional variable in each world. Equivalently φ can be understood as a function φ: Σ₀ → 2^W mapping each propositional atom to the set of worlds in which that atom holds.

The advantage of the latter is that φ can then be extended to the set Σ of all modal propositions by interpreting ∧ and ∨ as the respective set operations ∩ and ∪, and ¬X for any X⊆W as set difference W − X. Modalities are defined to make φ($\Diamond$ψ) (resp. φ($\Box$ψ)) the set of worlds s for which sRt holds for some (resp. all) world(s) t in φ(ψ). A formula that holds in all worlds is one that φ maps to W.

The article should also discuss the correspondence between modal logics such as K, T, S3, S4, S5, etc. and conditions on R involving reflexivity, transitivity, symmetry, etc. --Vaughan Pratt (talk) 06:28, 17 April 2011 (UTC)

I just noticed the link at the bottom to Kripke semantics, which covers all of the above. Since "Kripke structure" has the broader meaning covered in Kripke semantics, it would seem more appropriate to make this article simply a redirect to Kripke semantics and treat the model-checking application there. --Vaughan Pratt (talk) 06:32, 17 April 2011 (UTC)

I've added a hatnote for now. The addition of a set of initial states makes the definition not entirely equivalent, I believe, although this definition is not used universally in model checking literature. The article here might still be merged with model checking or temporal logic. —Ruud 09:36, 20 April 2011 (UTC)

It does seem that in model checking they extend the def with initial states. This page should be rename do Kripke structure (model checking), because it's not exactly the same thing. I suspect the extension/modification is notable enough for its own page, especially since they interpret it as an automaton. Tijfo098 (talk) 20:23, 20 April 2011 (UTC)

This article is confusing. What is AP in $L:S\rightarrow 2^{AP}$? There are less weird definitions of Kripke structure [1], granted not in the context of model checking. Tijfo098 (talk) 20:18, 20 April 2011 (UTC)

Apparently [2] someone copied the formulas wrong, or perhaps there was typo in Clarke et al. Tijfo098 (talk) 20:21, 20 April 2011 (UTC)

Atomic propositions. According to my lecture notes on model checking a Kripke structure is 5-tuple, which includes $AP$.

Clarke says "over AP", so it's clear what he means even if he doesn't include it in the tuple or notation. I've clarified that. Tijfo098 (talk) 15:49, 27 April 2011 (UTC)

Clarke is pretty annoying/sloppy textbook in general. They never seem to define state graph for instance, although they surely use the term a lot. Tijfo098 (talk) 15:56, 27 April 2011 (UTC)

Clarke manages to write a historical/introductory article without ever defining the notion, quite amusing: [3]. Tijfo098 (talk) 20:28, 20 April 2011 (UTC)

And this (extended notion) seems to be the same thing as a (labeled) state transition system. [4] [5]. Tijfo098 (talk) 20:32, 20 April 2011 (UTC)

The application/extension was definitely not discovered by Kripke [6]. Tijfo098 (talk) 20:39, 20 April 2011 (UTC)

Or, we can change the title of this page to Kripke structure (Model checking). Merging this article to temporal logic article is not a good idea. Kripke structure is in itself an important idea in the field of model checking. Ashutosh Gupta 20:41, 24 April 2011 (UTC)

I agree, merging with temporal logic is not a good idea. Perhaps merging with model checking might work, but I suspect it's too detailed to merge there. Renaming it to Kripke structure (model checking) and making Kripke structure a dab or {{SIA}} would probably work better. Tijfo098 (talk) 04:08, 25 April 2011 (UTC)

If nobody objects then we should make this change. Ashutosh Gupta (talk) 11:51, 26 April 2011 (UTC)