Talk:Kripke structure

From Wikipedia, the free encyclopedia

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)