MCMAS is an open-source model checker specialised in logics for multi-agent systems (MAS), in particular logics for strategic reasoning, but which at the moment can only handle qualitative objectives. We propose a first step towards extending MCMAS to certain quantitative strategic logics where the quantitative aspects have the form of energy constraints. We show that the existence of strategies for a coalition of agents for objectives given as a combination of LTL formula and bounded energy constraint can be reduced to the same problem for pure LTL objectives. Using this reduction, we run some experiments with MCMAS to solve quantitative strategic problems. Copyright © 2019 for this paper by its authors.
Towards a tool for LTL synthesis with bounded-energy constraints / Maubert, B.; Murano, A.; Perillo, P.; Rubin, S.; Spasiano, A.. - 2504:(2019), pp. 229-234. (Intervento presentato al convegno 20th Italian Conference on Theoretical Computer Science, ICTCS 2019).
Towards a tool for LTL synthesis with bounded-energy constraints
Maubert, B.;Murano, A.;Perillo, P.;Rubin, S.;Spasiano, A.
2019
Abstract
MCMAS is an open-source model checker specialised in logics for multi-agent systems (MAS), in particular logics for strategic reasoning, but which at the moment can only handle qualitative objectives. We propose a first step towards extending MCMAS to certain quantitative strategic logics where the quantitative aspects have the form of energy constraints. We show that the existence of strategies for a coalition of agents for objectives given as a combination of LTL formula and bounded energy constraint can be reduced to the same problem for pure LTL objectives. Using this reduction, we run some experiments with MCMAS to solve quantitative strategic problems. Copyright © 2019 for this paper by its authors.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
