×

zbMATH — the first resource for mathematics

An algebraic approach to multirelations and their properties. (English) Zbl 06696082
Summary: We study operations and equational properties of multirelations, which have been used for modelling games, protocols, computations, contact, closure and topology. The operations and properties are expressed using sets, heterogeneous relation algebras and more general algebras for multirelations. We investigate the algebraic properties of a new composition operation based on the correspondence to predicate transformers, different ways to express reflexive-transitive closures of multirelations, numerous equational properties, how these properties are connected and their preservation by multirelational operations. We particularly aim to generalise results and properties from up-closed multirelations to arbitrary multirelations. This paper is an extended version of [7].
MSC:
03 Mathematical logic and foundations
08 General algebraic systems
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aumann, G., Kontakt-relationen, (Sitzungsberichte der Bayerischen Akademie der Wissenschaften, (1970), Mathematisch-Naturwissenschaftliche Klasse), 67-77 · Zbl 0219.54001
[2] Aumann, G., Kontakt-relationen (2. mitteilung), (Sitzungsberichte der Bayerischen Akademie der Wissenschaften, (1971), Mathematisch-Naturwissenschaftliche Klasse), 119-122 · Zbl 0239.54001
[3] Aumann, G., Kontaktrelationen, Mathematisch-physikalische Semesterberichte zur Pflege des Zusammenhangs von Schule und Universität, vol. 20, 182-188, (1973) · Zbl 0272.54001
[4] Aumann, G., AD ARTEM ULTIMAM - eine einführung in die gedankenwelt der Mathematik, (1974), R. Oldenbourg Verlag · Zbl 0319.00002
[5] Back, R.-J.; von Wright, J., Refinement calculus, (1998), Springer New York
[6] Berghammer, R., Ordnungen, verbände und relationen mit anwendungen, (2012), Springer · Zbl 1254.06001
[7] Berghammer, R.; Guttmann, W., Closure, properties and closure properties of multirelations, (Jipsen, P.; Kahl, W.; Winter, M., RAMiCS 2015, Lect. Notes Comput. Sci., vol. 9348, (2015), Springer), 67-83 · Zbl 06527601
[8] Berghammer, R.; Guttmann, W., A relation-algebraic approach to multirelations and predicate transformers, (Hinze, R.; Voigtländer, J., MPC 2015, Lect. Notes Comput. Sci., vol. 9129, (2015), Springer), 50-70 · Zbl 1432.68069
[9] Berghammer, R.; Schmidt, G.; Zierer, H., Symmetric quotients and domain constructions, Inf. Process. Lett., 33, 3, 163-168, (1989) · Zbl 0689.68095
[10] Bird, R.; de Moor, O., Algebra of programming, (1997), Prentice Hall · Zbl 0867.68042
[11] Blanchette, J. C.; Böhme, S.; Paulson, L. C., Extending sledgehammer with SMT solvers, (Bjørner, N.; Sofronie-Stokkermans, V., CADE 2011, Lect. Notes Comput. Sci., vol. 6803, (2011), Springer), 116-130 · Zbl 1314.68271
[12] Blanchette, J. C.; Nipkow, T., Nitpick: a counterexample generator for higher-order logic based on a relational model finder, (Kaufmann, M.; Paulson, L. C., ITP 2010, Lect. Notes Comput. Sci., vol. 6172, (2010), Springer), 131-146 · Zbl 1291.68326
[13] Cavalcanti, A.; Woodcock, J.; Dunne, S., Angelic nondeterminism in the unifying theories of programming, Form. Asp. Comput., 18, 3, 288-307, (2006) · Zbl 1105.68012
[14] Fischer, M. J.; Ladner, R. E., Propositional dynamic logic of regular programs, J. Comput. Syst. Sci., 18, 2, 194-211, (1979) · Zbl 0408.03014
[15] Furusawa, H.; Kahl, W., A study on symmetric quotients, (1998), Fakultät für Informatik, Universität der Bundeswehr München, Technical Report 1998-06
[16] Furusawa, H.; Kawahara, Y.; Struth, G.; Tsumagari, N., Relational formalisations of compositions and liftings of multirelations, (Jipsen, P.; Kahl, W.; Winter, M., RAMiCS 2015, Lect. Notes Comput. Sci., vol. 9348, (2015), Springer), 84-100 · Zbl 06527602
[17] Furusawa, H.; Nishizawa, K.; Tsumagari, N., Multirelational models of lazy, monodic tree, and probabilistic Kleene algebras, Bull. Inform. Cybernet., 41, 11-24, (2009) · Zbl 1270.03137
[18] Furusawa, H.; Struth, G., Concurrent dynamic algebra, ACM Trans. Comput. Log., 16, 4, (2015) · Zbl 1367.03054
[19] Furusawa, H.; Struth, G., Taming multirelations, ACM Trans. Comput. Log., 17, 4, (2016) · Zbl 1407.03080
[20] Furusawa, H.; Tsumagari, N.; Nishizawa, K., A non-probabilistic relational model of probabilistic Kleene algebras, (Berghammer, R.; Möller, B.; Struth, G., RelMiCS/AKA 2008, Lect. Notes Comput. Sci., vol. 4988, (2008), Springer), 110-122 · Zbl 1140.68048
[21] Guttmann, W., Multirelations with infinite computations, J. Log. Algebraic Methods Program., 83, 2, 194-211, (2014) · Zbl 1371.68172
[22] Martin, C. E.; Curtis, S. A., The algebra of multirelations, Math. Struct. Comput. Sci., 23, 3, 635-674, (2013) · Zbl 1352.18001
[23] Martin, C. E.; Curtis, S. A.; Rewitzky, I., Modelling angelic and demonic nondeterminism with multirelations, Sci. Comput. Program., 65, 2, 140-158, (2007) · Zbl 1106.68023
[24] Möller, B., Kleene getting lazy, Sci. Comput. Program., 65, 2, 195-214, (2007) · Zbl 1109.68060
[25] Parikh, R., Propositional logics of programs: new directions, (Karpinski, M., FCT 1983, Lect. Notes Comput. Sci., vol. 158, (1983), Springer), 347-359
[26] Paulson, L. C.; Blanchette, J. C., Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers, (Sutcliffe, G.; Ternovska, E.; Schulz, S., Proceedings of the 8th International Workshop on the Implementation of Logics, (2010)), 3-13
[27] Peleg, D., Concurrent dynamic logic, J. ACM, 34, 2, 450-479, (1987) · Zbl 0645.03021
[28] Preoteasa, V., Algebra of monotonic Boolean transformers, (Simao, A.; Morgan, C., SBMF 2011, Lect. Notes Comput. Sci., vol. 7021, (2011), Springer), 140-155 · Zbl 1349.68051
[29] Rewitzky, I., Binary multirelations, (de Swart, H.; Orłowska, E.; Schmidt, G.; Roubens, M., TARSKI, Lect. Notes Comput. Sci., vol. 2929, (2003), Springer), 256-271 · Zbl 1203.68035
[30] Rewitzky, I.; Brink, C., Monotone predicate transformers as up-closed multirelations, (Schmidt, R., RelMiCS/AKA 2006, Lect. Notes Comput. Sci., vol. 4136, (2006), Springer), 311-327 · Zbl 1134.68390
[31] Schmidt, G., Partiality I: embedding relation algebras, J. Log. Algebraic Program., 66, 2, 212-238, (2006) · Zbl 1086.68093
[32] Schmidt, G., Relational mathematics, (2011), Cambridge University Press · Zbl 1214.06001
[33] Schmidt, G.; Berghammer, R., Contact, closure, topology, and the linking of row and column types of relations, J. Log. Algebraic Program., 80, 6, 339-361, (2011) · Zbl 1231.03058
[34] Schmidt, G.; Hattensperger, C.; Winter, M., Heterogeneous relation algebra, (Brink, C.; Kahl, W.; Schmidt, G., Relational Methods in Computer Science, (1997), Springer Wien), 39-53, chapter 3 · Zbl 0961.03061
[35] Schmidt, G.; Ströhlein, T., Relationen und graphen, (1989), Springer · Zbl 0705.68083
[36] Tarski, A., On the calculus of relations, J. Symb. Log., 6, 3, 73-89, (1941) · JFM 67.0973.02
[37] Tsumagari, N.; Nishizawa, K.; Furusawa, H., Multirelational model of lazy Kleene algebra, (Berghammer, R.; Möller, B.; Struth, G., Relations and Kleene Algebra in Computer Science: PhD Programme at RelMiCS10/AKA5, (2008), Institut für Informatik, Universität Augsburg), 73-77, Report 2008-04
[38] von Wright, J., Towards a refinement algebra, Sci. Comput. Program., 51, 1-2, 23-45, (2004) · Zbl 1091.68030
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.