Por Jaime Ramos (IST - Universidade de Lisboa).

The distributed temporal logic DTL is a logic for reasoning about temporal properties of distributed systems from the local point of view of the system's agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing.  In this talk, we propose an automata-theoretic model checking algorithm for DTL. To this end, we propose a notion of distributed transition system that will be used to specify the system to be verified. The properties that the system should meet are specified in DTL. In order to capture the models of these properties, we propose the notions of generalized distributed Buchi automaton and of distributed Buchi automaton. With these concepts, we are able to adapt results from automata-theoretic approaches to model checking in LTL to the distributed case. Then, we analyse the bounded model checking problem in the context of DTL. To this end, we adapt the bounded model checking algorithm for LTL to the case of DTL. To do so, a new notion of bounded semantics for DTL is proposed. In the bounded model checking approach, the witness problem is translated to the satisfiability of a propositional formula that can be addressed (efficiently) by SAT solvers.

Joint work with F. Dionísio, L. Viganò, F. Subtil and A. Peres.

Transmissão via Zoom.