Egalitarian state-transition systems (extended version)
| dc.contributor.author | Martín Sánchez, Óscar | |
| dc.contributor.author | Verdejo López, José Alberto | |
| dc.contributor.author | Martí Oliet, Narciso | |
| dc.date.accessioned | 2023-06-15T07:56:23Z | |
| dc.date.available | 2023-06-15T07:56:23Z | |
| dc.date.issued | 2016-08-28 | |
| dc.description | Tehcnical report 01/16 Departamento de Sistemas Informáticos y Computación Facultad de Informática | |
| dc.description.abstract | 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. | |
| dc.description.department | Depto. de Sistemas Informáticos y Computación | |
| dc.description.faculty | Fac. de Informática | |
| dc.description.refereed | FALSE | |
| dc.description.sponsorship | Ministerio de Economía y Competitividad (MINECO) | |
| dc.description.sponsorship | Comunidad de Madrid | |
| dc.description.status | unpub | |
| dc.eprint.id | https://eprints.ucm.es/id/eprint/38933 | |
| dc.identifier.uri | https://hdl.handle.net/20.500.14352/138.1 | |
| dc.language.iso | eng | |
| dc.page.total | 28 | |
| dc.relation.projectID | StrongSoft (TIN2012–39391– C04–04) | |
| dc.relation.projectID | N-GREENS Software (S2013/ICE-2731) | |
| dc.rights.accessRights | open access | |
| dc.subject.cdu | 004.4 | |
| dc.subject.keyword | state/transition structures TLR* model checking temporal logic Kripke structures LTS | |
| dc.subject.ucm | Informática (Informática) | |
| dc.subject.ucm | Software | |
| dc.subject.unesco | 1203.17 Informática | |
| dc.subject.unesco | 3304.16 Diseño Lógico | |
| dc.title | Egalitarian state-transition systems (extended version) | |
| dc.type | technical report | |
| dcterms.references | Bae, K., Meseguer, J.: The linear temporal logic of rewriting Maude model checker. WRLA 2010. LNCS, vol. 6381, pp. 208–225. Springer (2010) Bae, K., Meseguer, J.: A rewriting-based model checker for the linear temporal logic of rewriting. Electronic Notes in Theoretical Comp. Science 290, 19–36 (2012) Boudol, G., Castellani, I.: A non-interleaving semantics for CCS based on proved transitions. Fundamenta Informaticae 11, 433–452 (1988) Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM. LNCS, vol. 2999, pp. 128–147. Springer (2004) De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (Mar 1995) De Nicola, R., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) Semantics of Systems of Concurrent Processes. LNCS, vol. 469, pp. 407–419. Springer (1990) Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. WRLA 2002, ENTCS, vol. 71, pp. 162–187. Elsevier (2004) Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: On branching versus linear time temporal logic. J. ACM 33(1), 151–178 (Jan 1986) Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) Term Rewriting and Applications, RTA 2007, Proceedings. LNCS, vol. 4533, pp. 153–168. Springer (2007) Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1), 137–161 (1985) Kindler, E., Vesper, T.: Application and Theory of Petri Nets: ICATPN’98, chap. ESTL: A Temporal Logic for Events and States, pp. 365–384. Springer (1998) Kozen, D.: Results on the propositional ?-calculus. Theoretical Computer Science 27(3), 333–354 (1983) Martín, O., ?Verdejo, A., Martí-Oliet, N.: Model checking TLR* guarantee formulas on infinite systems. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software, LNCS, vol. 8373, pp. 129–150. Springer (2014) Martín, O., Verdejo, A., Martí-Oliet, N.: Egalitarian state-transition systems. In: International Workshop on Rewriting Logic and its Applications. pp. 98–117. Springer (2016) Martín, O., Verdejo, A., Martí-Oliet, N.: Synchronous products of rewrite systems. Tech. rep., Facultad de Informática, Universidad Complutense de Madrid (2016), http://maude.sip.ucm.es/syncprod Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992) Meseguer, J.: The temporal logic of rewriting: A gentle introduction. In: Degano, P., Nicola, R.D., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 354–382. Springer (2008) Reisig, W.: Petri Nets: An Introduction, EATCS Monographs on Theoretical Computer Science, vol. 4. Springer (1985) Sánchez, C., Samborski-Forlese, J.: Efficient regular linear temporal logic using dualization and stratification. TIME 2012 Proceedings, pp. 13–20. IEEE (2012) Wolper, P.: Temporal logic can be more expressive. Information and Control 56(1-2), 72–99 (1983) | |
| dspace.entity.type | Publication | |
| relation.isAuthorOfPublication | 556924eb-b77d-4d64-aed9-5a9e0eb0adb7 | |
| relation.isAuthorOfPublication | fdcba7f2-108a-46f4-bf49-c292a5b81953 | |
| relation.isAuthorOfPublication | e8d4e85a-2a43-444c-84e7-1fa5f392c50d | |
| relation.isAuthorOfPublication.latestForDiscovery | 556924eb-b77d-4d64-aed9-5a9e0eb0adb7 |
Download
Original bundle
1 - 1 of 1
