Synchronous products of rewrite 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-03 | |
| dc.description | Technical report 02/16 Departamento de Sistemas Informáticos y Computación Facultad de Informática Universidad Complutense de Madrid | |
| dc.description.abstract | We present and formalize a concept of synchronous product for rewrite systems, and also a corresponding concept for general transition systems, used as semantics for the former. A series of examples shows their practical usefulness: for the strategic control of systems, and for modular specification and verification. | |
| 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 | Comunidad de Madrid | |
| dc.description.sponsorship | Ministerio de Economía y Competitividad (MINECO) | |
| dc.description.status | unpub | |
| dc.eprint.id | https://eprints.ucm.es/id/eprint/39856 | |
| dc.identifier.uri | https://hdl.handle.net/20.500.14352/139.1 | |
| dc.language.iso | eng | |
| dc.page.total | 22 | |
| dc.relation.projectID | N-GREENS Software (S2013/ICE-2731) | |
| dc.relation.projectID | StrongSoft (TIN2012--39391--C04–04) | |
| dc.rights.accessRights | open access | |
| dc.subject.cdu | 004.4 | |
| dc.subject.keyword | Synchronous product | |
| dc.subject.keyword | parallel composition | |
| dc.subject.keyword | rewriting logic strategies Maude transition systems modular specification modular verification | |
| 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 | Synchronous products of rewrite systems (extended version) | |
| dc.type | technical report | |
| dcterms.references | Bae, K., Meseguer, J.: The linear temporal logic of rewriting Maude model checker. In: Olveczky, P.C. (ed.) Rewriting Logic and its Applications. WRLA 2010, Revised Selected Papers. LNCS, vol. 6381, pp. 208--225. Springer (2010) Borovansky, P., Kirchner, C., Kirchner, H., Moreau, P.E.: ELAN from a rewriting logic point of view. TCS 285(2), 155--185 (2002) Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001) Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Logic in Computer Science. Proceedings of LICS 1989, pp. 353--362 (Jun 1989) Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude - A High-Performance Logical Framework, LNCS, vol. 4350. Springer (2007) Durán, F., Meseguer, J.: The Maude specification of Full Maude (Feb 1999), \url{http://maude.cs.uiuc.edu/papers}, manuscript, Computer Science Laboratory, SRI International Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds.) Proceedings of WRLA 2002, ENTCS, vol.~71, pp. 162--187. Elsevier (2004) 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) Harel, D., Lampert, R., Marron, A., Weiss, G.: Model-checking behavioral programs. In: Proceedings of EMSOFT '11, ACM, 2011 Harel, D., Marron, A., Weiss, G.: Behavioral programming. Commun. ACM 55(7), 90--100 (Jul 2012) Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: Feather, M.S., Goedicke, M. (eds.) Proceedings ASE 2001. pp. 135--143. IEEE (2001) Kirchner, H.: Rewriting strategies and strategic rewrite programs. In: Martí-Oliet, N., Olveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency, LNCS, vol. 9200, pp. 380--403. Springer International Publishing (2015) Kupferman, O., Vardi, M.Y.: An automata-theoretic approach to modular model checking. ACM Trans. Program. Lang. Syst. 22(1), 87--128 (Jan 2000) Martí-Oliet, N., Meseguer, J., Verdejo, A.: A rewriting semantics for Maude strategies. In: Rosu, G. (ed.) Proceedings of WRLA 2008. ENTCS, vol. 238(3), pp. 227--247. Elsevier (2009) {Martín, Ó., Verdejo, A., Martí-Oliet, N.: Egalitarian state-transition systems (2016), \url{http://maude.sip.ucm.es/syncprod}, submitted Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. TCS 96(1), 73--155 (1992) Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) Recent Trends in Algebraic Development Techniques, WADT'97. LNCS, vol. 1376, pp. 18--61. Springer (1997) 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) Milner, R.: A Calculus of Communicating Systems, LNCS, vol. 92. Springer (1980) Plump, D.: The design of {GP} 2. In: Escobar, S. (ed.) Proceedings of WRS 2011. EPTCS, vol.~82, pp. 1--16 (2011) Poskitt, C.M., Plump, D.: {Hoare}-style verification of graph programs. Fundamenta Informaticae 118(1-2), 135--175 (2012) Roldán, M., Durán, F., Vallecillo, A.: Invariant-driven specifications in {Maude}. Science of Computer Programming 74(10), 812--835 (2009) Visser, E.: A survey of rewriting strategies in program transformation systems. WRS 2001 ENTCS 57, 109--143 (2001) | |
| 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
