A Kripke structure is a type of nondeterministic finite state machine proposed by Saul Kripke in 1963, used in model checking to represent the behaviour of a system. It is basically a graph whose nodes represent the reachable states of the system and whose edges represent state transitions. A labeling function maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures.

PropertyValue
dbpprop:abstract
  • A Kripke structure is a type of nondeterministic finite state machine proposed by Saul Kripke in 1963, used in model checking to represent the behaviour of a system. It is basically a graph whose nodes represent the reachable states of the system and whose edges represent state transitions. A labeling function maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures.
  • Une structure de Kripke est une sorte d'automate fini non-déterministe utilisé par exemple dans le model checking pour représenter le comportement d'un système. C'est un graphe orienté dont les nœuds représentent les états accessibles du système et dont les arcs représentent les transitions entre les états. Une fonction d'étiquetage fait correspondre à chaque état un ensemble de propositions logiques vraies dans cet état. Les logiques temporelles sont généralement interprétées dans des structures de Kripke.
dbpprop:hasPhotoCollection
rdfs:comment
  • A Kripke structure is a type of nondeterministic finite state machine proposed by Saul Kripke in 1963, used in model checking to represent the behaviour of a system. It is basically a graph whose nodes represent the reachable states of the system and whose edges represent state transitions. A labeling function maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures.
  • Une structure de Kripke est une sorte d'automate fini non-déterministe utilisé par exemple dans le model checking pour représenter le comportement d'un système. C'est un graphe orienté dont les nœuds représentent les états accessibles du système et dont les arcs représentent les transitions entre les états. Une fonction d'étiquetage fait correspondre à chaque état un ensemble de propositions logiques vraies dans cet état.
rdfs:label
  • Kripke structure
  • Structure de Kripke
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of