4 papers
Towards Probabilistic Strategic Timed CTL
Wojciech Jamroga, Marta Kwiatkowska, Wojciech Penczek +2
We define PSTCTL, a probabilistic variant of Strategic Timed CTL (STCTL), interpreted over stochastic multi-agent systems with continuous time and asynchronous execution semantics.…
IMITATOR4AMAS: Strategy Synthesis for STCTL
Davide Catta, Adrien Lacroix, Wojciech Penczek +2
IMITATOR4AMAS supports model checking and synthesis of memoryless imperfect information strategies for STCTL, interpreted over networks of parametric timed automata with asynchrono…
Practical Abstractions for Model Checking Continuous-Time Multi-Agent Systems
Yan Kim, Wojciech Jamroga, Wojciech Penczek +1
Model checking of temporal logics in a well established technique to verify and validate properties of multi-agent systems (MAS). However, practical model checking requires input m…
A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
Jaime Arias, Kyungmin Bae, Carlos Olarte +2
This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where paramet…