Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: temporal epistemic logic

Sortuj według:

Ogranicz wyniki do:

Model Checking Temporal-Epistemic Logic Using Alternating Tree Automata

Belardinelli F., Jones A. V., Lomuscio A.

Fundamenta Informaticae

2011

Vol. 112, nr 1

19-37

We introduce a novel automata-theoretic approach for the verification of multi-agent systems. We present epistemic alternating tree automata, an extension of alternating tree automata, and use them to represent specifications in the temporal-epistemic logic CTLK. We show that model checking a memory-less interpreted system against a CTLK property can be reduced to checking the language non-emptiness of the composition of two epistemic tree automata. We report on an experimental implementation and discuss preliminary results. We evaluate the effectiveness of the technique using two real-life scenarios: a gossip protocol and the train gate controller.

From Bounded to Unbounded Model Checking for Temporal Epistemic Logic

Kacprzak M., Lomuscio A., Penczek W.

Fundamenta Informaticae

2004

Vol. 63, nr 2,3

221--240

This paper addresses the problem of verification of temporal epistemic properties of multi-agent systems by means of symbolic model checking. An overview of the technique of bounded model checking for temporal epistemic logic, and an analysis of some limitations of the method are provided. An extension of this technique called unbounded model checking to solve these limitations is explored. Similarities and differences of the two methods are explicitly exemplified by the analysis of a scenario in the two formalisms.