×

Egalitarian state-transition systems. (English) Zbl 1367.68198

Lucanu, Dorel (ed.), Rewriting logic and its applications. 11th international workshop, WRLA 2016, held as a satellite event of ETAPS, Eindhoven, The Netherlands, April 2–3, 2016. Revised selected papers. Cham: Springer (ISBN 978-3-319-44801-5/pbk; 978-3-319-44802-2/ebook). Lecture Notes in Computer Science 9942, 98-117 (2016).
Summary: 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 strategy expressions 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.
For the entire collection see [Zbl 1344.68013].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68Q42 Grammars and rewriting systems

Software:

Maude
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bae, K., Meseguer, J.: The linear temporal logic of rewriting Maude model checker. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 208–225. Springer, Heidelberg (2010) · Zbl 1306.68099 · doi:10.1007/978-3-642-16310-4_14
[2] Bae, K., Meseguer, J.: A rewriting-based model checker for the linear temporal logic of rewriting. In: Kniesel, G., Pinto, J.S. (eds.) Rule 2008. ENTCS, vol. 290, pp. 19–36. Elsevier (2012) · Zbl 1291.68244 · doi:10.1016/j.entcs.2012.11.009
[3] Boudol, G., Castellani, I.: A non-interleaving semantics for CCS based on proved transitions. Fundamenta Informaticae 11, 433–452 (1988) · Zbl 0657.68066
[4] 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.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 128–147. Springer, Heidelberg (2004) · Zbl 1196.68129 · doi:10.1007/978-3-540-24756-2_8
[5] De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (1995) · Zbl 0886.68064 · doi:10.1145/201019.201032
[6] 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, Heidelberg (1990) · doi:10.1007/3-540-53479-2_17
[7] Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds.) WRLA 2002. ENTCS, vol. 71, pp. 162–187. Elsevier (2004) · Zbl 1272.68243 · doi:10.1016/S1571-0661(05)82534-4
[8] Emerson, E.A., Halpern, J.Y.: ”Sometimes” and ”not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986) · Zbl 0629.68020 · doi:10.1145/4904.4999
[9] Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153–168. Springer, Heidelberg (2007) · Zbl 1203.68097 · doi:10.1007/978-3-540-73449-9_13
[10] Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985) · Zbl 0629.68021 · doi:10.1145/2455.2460
[11] Kindler, E., Vesper, T.: ESTL: a temporal logic for events and states. In: Desel, J., Silva, M. (eds.) ICATPN 1998. LNCS, vol. 1420, pp. 365–384. Springer, Heidelberg (1998) · doi:10.1007/3-540-69108-1_20
[12] Kozen, D.: Results on the propositional \[ \mu \] -calculus. TCS 27(3), 333–354 (1983) · Zbl 0553.03007 · doi:10.1016/0304-3975(82)90125-6
[13] Martín, Ó., 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, Heidelberg (2014) · Zbl 1407.68296 · doi:10.1007/978-3-642-54624-2_7
[14] Martín, Ó., Verdejo, A., Martí-Oliet, N.: Synchronous products of rewrite systems. Technical report, Facultad de Informática, Universidad Complutense de Madrid (2016). http://maude.sip.ucm.es/syncprod · Zbl 1367.68198
[15] Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. TCS 96(1), 73–155 (1992) · Zbl 0758.68043 · doi:10.1016/0304-3975(92)90182-F
[16] Meseguer, J.: The temporal logic of rewriting: a gentle introduction. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 354–382. Springer, Heidelberg (2008) · Zbl 1143.68459 · doi:10.1007/978-3-540-68679-8_22
[17] Reisig, W.: Petri Nets: An Introduction. EATCS Monographs on TCS, vol. 4. Springer, Heidelberg (1985) · Zbl 0555.68033 · doi:10.1007/978-3-642-69968-9
[18] Sánchez, C., Samborski-Forlese, J.: Efficient regular linear temporal logic using dualization and stratification. In: Reynolds, M., Terenziani, P., Moszkowski, B. (eds.) Proceedings of TIME 2012, pp. 13–20. IEEE (2012) · doi:10.1109/TIME.2012.25
[19] Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1–2), 72–99 (1983) · Zbl 0534.03009 · doi:10.1016/S0019-9958(83)80051-5
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.