| dbo:abstract
|
- Η δομή Κρίπκε (Αγγλικά: Kripke structure) είναι ένας τύπος μη-ντετερμινιστικής μηχανής πεπερασμένων καταστάσεων που προτάθηκε από τον Σάουλ Κρίπκε το 1963 και χρησιμοποιείται στον έλεγχο μοντέλων για να αναπαριστά τη συμπεριφορά ενός συστήματος. Αποτελείται από ένα γράφο, οι κόμβοι του οποίου αναπαριστούν τις προσβάσιμες καταστάσεις του συστήματος και οι ακμές του τις μεταβάσεις μεταξύ καταστάσεων. Μια συνάρτηση απόδοσης ετικετών (labeling function) αντιστοιχεί σε κάθε κόμβο ένα σύνολο από ιδιότητες που ισχύουν σε μια συγκεκριμένη κατάσταση. Οι χρονικές λογικές συνήθως ερμηνεύονται με δομές Κρίπκε. (el)
- Una estructura de Kripke es una variación del , originalmente propuesta por Saul Kripke, usada en Verificación de modelos. para representar el comportamiento de un sistema. Es básicamente un grafo cuyos nodos representan estados alcanzables del sistema y cuyas aristas representan transiciones de estados. Una función de etiquetado mapea cada nodo a un conjunto de propiedades que se cumple en el estado correspondiente. Las lógicas temporales son interpretadas tradicionalmente en términos de estructuras de Kripke. (es)
- A Kripke structure is a variation of the transition system, originally proposed by Saul Kripke, used in model checking to represent the behavior of a system.It consists of a graph whose nodes represent the reachable states of the system and whose edges represent state transitions, together with a labelling function which maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures. (en)
- Une structure de Kripke est un modèle de calcul, proche d'un automate fini non déterministe, inventé par Saul Kripke. Elle est utilisée 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. L'existence de certains chemins dans le graphe est alors considérée comme une éventualité de réalisation de formules. (fr)
- I modelli di Kripke sono creati da Saul Kripke per descrivere "":
* con infiniti comportamenti (Protocolli di comunicazione, circuiti hardware, ...);
* Rappresentano l'evoluzione dinamica dei ;
* Uno stato include i valori di variabili di stato, il programma contatori, i contenuti dei canali di comunicazione;
* Possono essere animati e convalidati prima della loro effettiva attuazione. (it)
- 크립키 구조(Kripke Structure)는 논리학자 솔 크립키가 1963년 제안한, 비결정 유한 상태 오토마타의 일종이다. 에서 시스템의 움직임을 기술하는데 사용된다. 크립키 구조는 접근 가능한 상태(state)들을 나타내는 노드(node)와, 상태 전이(state transition)을 나타내는 엣지로 구성된 그래프의 모양이다. 여기에 각 노드에 매핑되는 라벨 함수(labelling function)이 있어, 어떤 상태에 대해 어떤 속성값들의 집합을 대응시킨다. 시간 논리의 주요 논리 구조들은 크립키 구조로 기술되고 있다. (ko)
- Model Kripkego (nazywany również modelem relacyjnym) – struktura matematyczna używana w logikach modalnych i intuicjonistycznym rachunku zdań. Definiuje się go jako trójkę gdzie to zbiór niepusty, – relacja na tym zbiorze (podzbiór właściwy iloczynu kartezjańskiego ), a – funkcją przyporządkowującą kolejnym zmiennym zdaniowym podzbiory zbioru Nazwa pochodzi od nazwiska pioniera badań nad semantyką relacyjną Saula Aarona Kripkego. (pl)
- Модель Крипке (англ. Kripke structure) — это один из вариантов недетерминированного конечного автомата, который был предложен Солом Крипке. Этот вид НКА применяется при проверке моделей для представления поведения системы. Модель Крипке является простой абстрактной машиной, позволяющей описать идеи вычислительной машины без добавления особых сложностей. Модель представляется ориентированным графом, вершины которого описывают достижимые состояния системы, а ребра — переходы из состояния в состояние. Функция пометок сопоставляет каждой вершине множество свойств, которые выполняются в соответствующем состоянии. (ru)
- 克里普克结构（或称Kripke结构）是迁移系统的一个变种，最初由索尔·克里普克提出，用于在中表示一个系统的行为。克里普克结构本身是一个图，其结点表示系统可达的状态，其边表示状态的迁移。 有一个标号函数将结点与结点所具有的性质的集合映射起来。时序逻辑传统上是由克里普克结构进行解释的。 (zh)
|
| dbo:thumbnail
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 6169 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:wikiPageUsesTemplate
| |
| dcterms:subject
| |
| rdf:type
| |
| rdfs:comment
|
- Η δομή Κρίπκε (Αγγλικά: Kripke structure) είναι ένας τύπος μη-ντετερμινιστικής μηχανής πεπερασμένων καταστάσεων που προτάθηκε από τον Σάουλ Κρίπκε το 1963 και χρησιμοποιείται στον έλεγχο μοντέλων για να αναπαριστά τη συμπεριφορά ενός συστήματος. Αποτελείται από ένα γράφο, οι κόμβοι του οποίου αναπαριστούν τις προσβάσιμες καταστάσεις του συστήματος και οι ακμές του τις μεταβάσεις μεταξύ καταστάσεων. Μια συνάρτηση απόδοσης ετικετών (labeling function) αντιστοιχεί σε κάθε κόμβο ένα σύνολο από ιδιότητες που ισχύουν σε μια συγκεκριμένη κατάσταση. Οι χρονικές λογικές συνήθως ερμηνεύονται με δομές Κρίπκε. (el)
- Una estructura de Kripke es una variación del , originalmente propuesta por Saul Kripke, usada en Verificación de modelos. para representar el comportamiento de un sistema. Es básicamente un grafo cuyos nodos representan estados alcanzables del sistema y cuyas aristas representan transiciones de estados. Una función de etiquetado mapea cada nodo a un conjunto de propiedades que se cumple en el estado correspondiente. Las lógicas temporales son interpretadas tradicionalmente en términos de estructuras de Kripke. (es)
- A Kripke structure is a variation of the transition system, originally proposed by Saul Kripke, used in model checking to represent the behavior of a system.It consists of a graph whose nodes represent the reachable states of the system and whose edges represent state transitions, together with a labelling function which maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures. (en)
- Une structure de Kripke est un modèle de calcul, proche d'un automate fini non déterministe, inventé par Saul Kripke. Elle est utilisée 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. L'existence de certains chemins dans le graphe est alors considérée comme une éventualité de réalisation de formules. (fr)
- I modelli di Kripke sono creati da Saul Kripke per descrivere "":
* con infiniti comportamenti (Protocolli di comunicazione, circuiti hardware, ...);
* Rappresentano l'evoluzione dinamica dei ;
* Uno stato include i valori di variabili di stato, il programma contatori, i contenuti dei canali di comunicazione;
* Possono essere animati e convalidati prima della loro effettiva attuazione. (it)
- 크립키 구조(Kripke Structure)는 논리학자 솔 크립키가 1963년 제안한, 비결정 유한 상태 오토마타의 일종이다. 에서 시스템의 움직임을 기술하는데 사용된다. 크립키 구조는 접근 가능한 상태(state)들을 나타내는 노드(node)와, 상태 전이(state transition)을 나타내는 엣지로 구성된 그래프의 모양이다. 여기에 각 노드에 매핑되는 라벨 함수(labelling function)이 있어, 어떤 상태에 대해 어떤 속성값들의 집합을 대응시킨다. 시간 논리의 주요 논리 구조들은 크립키 구조로 기술되고 있다. (ko)
- Model Kripkego (nazywany również modelem relacyjnym) – struktura matematyczna używana w logikach modalnych i intuicjonistycznym rachunku zdań. Definiuje się go jako trójkę gdzie to zbiór niepusty, – relacja na tym zbiorze (podzbiór właściwy iloczynu kartezjańskiego ), a – funkcją przyporządkowującą kolejnym zmiennym zdaniowym podzbiory zbioru Nazwa pochodzi od nazwiska pioniera badań nad semantyką relacyjną Saula Aarona Kripkego. (pl)
- 克里普克结构（或称Kripke结构）是迁移系统的一个变种，最初由索尔·克里普克提出，用于在中表示一个系统的行为。克里普克结构本身是一个图，其结点表示系统可达的状态，其边表示状态的迁移。 有一个标号函数将结点与结点所具有的性质的集合映射起来。时序逻辑传统上是由克里普克结构进行解释的。 (zh)
- Модель Крипке (англ. Kripke structure) — это один из вариантов недетерминированного конечного автомата, который был предложен Солом Крипке. Этот вид НКА применяется при проверке моделей для представления поведения системы. Модель Крипке является простой абстрактной машиной, позволяющей описать идеи вычислительной машины без добавления особых сложностей. Модель представляется ориентированным графом, вершины которого описывают достижимые состояния системы, а ребра — переходы из состояния в состояние. (ru)
|
| rdfs:label
|
- Δομή Κρίπκε (el)
- Estructura de Kripke (es)
- Modelli di Kripke (it)
- Structure de Kripke (fr)
- Kripke structure (model checking) (en)
- 크립키 구조 (ko)
- Model Kripkego (pl)
- Модель Крипке (ru)
- 克里普克结构 (zh)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:depiction
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:wikiPageRedirects
of | |
| is dbo:wikiPageWikiLink
of | |
| is foaf:primaryTopic
of | |
