Kripke structure (model checking)
http://dbpedia.org/resource/Kripke_structure_(model_checking) an entity of type: Abstraction100002137
Η δομή Κρίπκε (Αγγλικά: Kripke structure) είναι ένας τύπος μη-ντετερμινιστικής μηχανής πεπερασμένων καταστάσεων που προτάθηκε από τον Σάουλ Κρίπκε το 1963 και χρησιμοποιείται στον έλεγχο μοντέλων για να αναπαριστά τη συμπεριφορά ενός συστήματος. Αποτελείται από ένα γράφο, οι κόμβοι του οποίου αναπαριστούν τις προσβάσιμες καταστάσεις του συστήματος και οι ακμές του τις μεταβάσεις μεταξύ καταστάσεων. Μια συνάρτηση απόδοσης ετικετών (labeling function) αντιστοιχεί σε κάθε κόμβο ένα σύνολο από ιδιότητες που ισχύουν σε μια συγκεκριμένη κατάσταση. Οι χρονικές λογικές συνήθως ερμηνεύονται με δομές Κρίπκε.
rdf:langString
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.
rdf:langString
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.
rdf:langString
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.
rdf:langString
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.
rdf:langString
크립키 구조(Kripke Structure)는 논리학자 솔 크립키가 1963년 제안한, 비결정 유한 상태 오토마타의 일종이다. 에서 시스템의 움직임을 기술하는데 사용된다. 크립키 구조는 접근 가능한 상태(state)들을 나타내는 노드(node)와, 상태 전이(state transition)을 나타내는 엣지로 구성된 그래프의 모양이다. 여기에 각 노드에 매핑되는 라벨 함수(labelling function)이 있어, 어떤 상태에 대해 어떤 속성값들의 집합을 대응시킨다. 시간 논리의 주요 논리 구조들은 크립키 구조로 기술되고 있다.
rdf:langString
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.
rdf:langString
克里普克结构（或称Kripke结构）是迁移系统的一个变种，最初由索尔·克里普克提出，用于在中表示一个系统的行为。克里普克结构本身是一个图，其结点表示系统可达的状态，其边表示状态的迁移。 有一个标号函数将结点与结点所具有的性质的集合映射起来。时序逻辑传统上是由克里普克结构进行解释的。
rdf:langString
Модель Крипке (англ. Kripke structure) — это один из вариантов недетерминированного конечного автомата, который был предложен Солом Крипке. Этот вид НКА применяется при проверке моделей для представления поведения системы. Модель Крипке является простой абстрактной машиной, позволяющей описать идеи вычислительной машины без добавления особых сложностей. Модель представляется ориентированным графом, вершины которого описывают достижимые состояния системы, а ребра — переходы из состояния в состояние.
rdf:langString
rdf:langString
Δομή Κρίπκε
rdf:langString
Estructura de Kripke
rdf:langString
Modelli di Kripke
rdf:langString
Structure de Kripke
rdf:langString
Kripke structure (model checking)
rdf:langString
크립키 구조
rdf:langString
Model Kripkego
rdf:langString
Модель Крипке
rdf:langString
克里普克结构
xsd:integer
1591127
xsd:integer
1068734877
rdf:langString
Η δομή Κρίπκε (Αγγλικά: Kripke structure) είναι ένας τύπος μη-ντετερμινιστικής μηχανής πεπερασμένων καταστάσεων που προτάθηκε από τον Σάουλ Κρίπκε το 1963 και χρησιμοποιείται στον έλεγχο μοντέλων για να αναπαριστά τη συμπεριφορά ενός συστήματος. Αποτελείται από ένα γράφο, οι κόμβοι του οποίου αναπαριστούν τις προσβάσιμες καταστάσεις του συστήματος και οι ακμές του τις μεταβάσεις μεταξύ καταστάσεων. Μια συνάρτηση απόδοσης ετικετών (labeling function) αντιστοιχεί σε κάθε κόμβο ένα σύνολο από ιδιότητες που ισχύουν σε μια συγκεκριμένη κατάσταση. Οι χρονικές λογικές συνήθως ερμηνεύονται με δομές Κρίπκε.
rdf:langString
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.
rdf:langString
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.
rdf:langString
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.
rdf:langString
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.
rdf:langString
크립키 구조(Kripke Structure)는 논리학자 솔 크립키가 1963년 제안한, 비결정 유한 상태 오토마타의 일종이다. 에서 시스템의 움직임을 기술하는데 사용된다. 크립키 구조는 접근 가능한 상태(state)들을 나타내는 노드(node)와, 상태 전이(state transition)을 나타내는 엣지로 구성된 그래프의 모양이다. 여기에 각 노드에 매핑되는 라벨 함수(labelling function)이 있어, 어떤 상태에 대해 어떤 속성값들의 집합을 대응시킨다. 시간 논리의 주요 논리 구조들은 크립키 구조로 기술되고 있다.
rdf:langString
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.
rdf:langString
Модель Крипке (англ. Kripke structure) — это один из вариантов недетерминированного конечного автомата, который был предложен Солом Крипке. Этот вид НКА применяется при проверке моделей для представления поведения системы. Модель Крипке является простой абстрактной машиной, позволяющей описать идеи вычислительной машины без добавления особых сложностей. Модель представляется ориентированным графом, вершины которого описывают достижимые состояния системы, а ребра — переходы из состояния в состояние. Функция пометок сопоставляет каждой вершине множество свойств, которые выполняются в соответствующем состоянии.
rdf:langString
克里普克结构（或称Kripke结构）是迁移系统的一个变种，最初由索尔·克里普克提出，用于在中表示一个系统的行为。克里普克结构本身是一个图，其结点表示系统可达的状态，其边表示状态的迁移。 有一个标号函数将结点与结点所具有的性质的集合映射起来。时序逻辑传统上是由克里普克结构进行解释的。
xsd:nonNegativeInteger
6169
