RT Report
T1 Egalitarian state-transition systems (extended version)
A1 Martín Sánchez, Óscar
A1 Verdejo López, José Alberto
A1 Martí Oliet, Narciso
AB We argue that considering transitions at the same level as states, as first-class citizens, is advantageous in many cases. Namely, the use of atomic propositions on transitions, as well as on states, allows temporal formulas and strategies to be more powerful, general, and meaningful. We define egalitarian structures and logics, and show how they generalize well-known state-based, event-based, and mixed ones. We present translations from egalitarian to non-egalitarian settings that, in particular, allow the model checking of LTLR formulas using Maude’s LTL model checker. We have implemented these translations as a prototype in Maude itself.
YR 2016
FD 2016-08-28
LK https://hdl.handle.net/20.500.14352/138.1
UL https://hdl.handle.net/20.500.14352/138.1
LA eng
NO Tehcnical report 01/16Departamento de Sistemas Informáticos y ComputaciónFacultad de Informática
NO Ministerio de Economía y Competitividad (MINECO)
NO Comunidad de Madrid
DS Docta Complutense
RD 14 abr 2025