Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

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.