×

Characterizing right inverses for spatial constraint systems with applications to modal logic. (English) Zbl 1400.68134

Summary: Spatial constraint systems are algebraic structures from concurrent constraint programming to specify spatial and epistemic behavior in multi-agent systems. In this paper spatial constraint systems are used to give an abstract characterization of the notion of normality in modal logic and to derive right inverse/reverse operators for modal languages. In particular, a necessary and sufficient condition for the existence of right inverses is identified and the abstract notion of normality is shown to correspond to the preservation of finite suprema. Furthermore, a taxonomy of normal right inverses is provided, identifying the greatest normal right inverse as well as the complete family of minimal right inverses. These results are applied to existing modal languages such as the weakest normal modal logic, Hennessy-Milner logic, and linear-time temporal logic. Some implications of these results are also discussed in the context of modal concepts such as bisimilarity and inconsistency invariance.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B45 Modal logic (including the logic of norms)
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Knight, S.; Palamidessi, C.; Panangaden, P.; Valencia, F. D., Spatial and epistemic modalities in constraint-based process calculi, (CONCUR 2012, LNCS, vol. 7454, (2012), Springer), 317-332 · Zbl 1364.68290
[2] Saraswat, V. A.; Rinard, M.; Panangaden, P., Semantic foundations of concurrent constraint programming, (POPL’91, (1991), ACM), 333-352
[3] Boer, F. S.; Di Pierro, A.; Palamidessi, C., Nondeterminism and infinite computations in constraint programming, Theoret. Comput. Sci., 37-78, (1995) · Zbl 0872.68103
[4] Fages, F.; Ruet, P.; Soliman, S., Linear concurrent constraint programming: operational and phase semantics, Inform. and Comput., 14-41, (2001) · Zbl 1003.68065
[5] Réty, J., Distributed concurrent constraint programming, Fund. Inform., 323-346, (1998) · Zbl 0943.68025
[6] Nielsen, M.; Palamidessi, C.; Valencia, F. D., Temporal concurrent constraint programming: denotation, logic and applications, Nordic J. Comput., 9, 1, 145-188, (2002) · Zbl 1018.68019
[7] Popkorn, S., First steps in modal logic, (1994), Cambridge University Press · Zbl 0921.03019
[8] Ryan, M.; Schobbens, P.-Y., Counterfactuals and updates as inverse modalities, J. Log. Lang. Inf., 123-146, (1997) · Zbl 0921.03035
[9] Haar, S.; Perchy, S.; Rueda, C.; Valencia, F. D., An algebraic view of space/belief and extrusion/utterance for concurrency/epistemic logic, (PPDP 2015, (2015), ACM), 161-172
[10] Phillips, I.; Ulidowski, I., A logic with reverse modalities for history-preserving bisimulations, (EXPRESS’11, EPTCS, vol. 64, (2011)), 104-118
[11] Fagin, R.; Halpern, J. Y.; Moses, Y.; Vardi, M. Y., Reasoning about knowledge, (1995), MIT Press Cambridge · Zbl 0839.68095
[12] Pnueli, A.; Manna, Z., The temporal logic of reactive and concurrent systems, (1992), Springer
[13] Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. ACM (JACM), 32, 1, 137-161, (1985) · Zbl 0629.68021
[14] Hintikka, J., Knowledge and belief, (1962), Cornell University Press
[15] Vickers, S., Topology via logic, (1996), Cambridge University Press · Zbl 0922.54002
[16] Guzman, M.; Perchy, S.; Rueda, C.; Valencia, F., Deriving inverse operators for modal logic, (Theoretical Aspects of Computing - ICTAC 2016, LNCS, vol. 9965, (2016), Springer), 214-232 · Zbl 1482.68153
[17] Haar, S.; Perchy, S.; Rueda, C.; Valencia, F., An algebraic view of space/belief and extrusion/utterance for concurrency/epistemic logic, (17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015, (2015), ACM SIGPLAN), 161-172
[18] Guzman, M.; Haar, S.; Perchy, S.; Rueda, C.; Valencia, F. D., Belief, knowledge, lies and other utterances in an algebra for space and extrusion, J. Log. Algebraic Methods Program., 86, 1, 107-133, (2017) · Zbl 1353.68203
[19] Abramsky, S.; Jung, A., Domain theory, (Abramsky, S.; etal., Handbook of Logic in Computer Science, vol. 3, (1994), Oxford University Press), 1-168
[20] Blackburn, P.; De Rijke, M.; Venema, Y., Modal logic, (2002), Cambridge University Press
[21] Aristizábal, A.; Bonchi, F.; Palamidessi, C.; Pino, L.; Valencia, Frank D., Deriving labels and bisimilarity for concurrent constraint programming, (Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2011, LNCS, (2011), Springer), 138-152 · Zbl 1326.68196
[22] Prior, A. N., Past, present and future, vol. 154, (1967), Oxford University Press · Zbl 0169.29802
[23] Knight, S., The epistemic view of concurrency theory, (2013), École Polytechnique Palaiseau, France, Ph.D. thesis
[24] Milner, R., Communication and concurrency, vol. 84, (1989), Prentice Hall New York etc.
[25] Macnab, D., Modal operators on Heyting algebras, Algebra Universalis, 12, 1, 5-29, (1981) · Zbl 0459.06005
[26] Chagrov, A.; Zakharyaschev, M., Modal logic, Oxford Logic Guides, vol. 35, (1997) · Zbl 0871.03007
[27] De Nicola, R.; Ferrari, G. L., Observational logics and concurrency models, (FSTTCS’90, LNCS, vol. 472, (1990), Springer), 301-315
[28] Goltz, U.; Kuiper, R.; Penczek, W., Propositional temporal logics and equivalences, (CONCUR’92, LNCS, vol. 630, (1992), Springer), 222-236
[29] De Nicola, R.; Montanari, U.; Vaandrager, F., Back and forth bisimulations, (CONCUR ’90, LNCS, vol. 458, (1990), Springer), 152-165
[30] De Nicola, R.; Vaandrager, F., Three logics for branching bisimulation, J. ACM (JACM), 42, 2, 458-487, (1995) · Zbl 0886.68064
[31] Blyth, T.; Janowitz, M., Residuation theory, International Series of Monographs in Pure and Applied Mathematics, vol. 102, (1972), Pergamon Press Oxford · Zbl 0301.06001
[32] Gadducci, F.; Santini, F.; Pino, L. F.; Valencia, F. D., A labelled semantics for soft concurrent constraint programming, (International Conference on Coordination Languages and Models, (2015), Springer), 133-149
[33] Palamidessi, C.; Saraswat, V.; Valencia, F. D.; Victor, B., On the expressiveness of linearity vs persistence in the asynchronous pi-calculus, (Twenty First Annual IEEE Symposium on Logic in Computer Science (LICS), (2006), IEEE Computer Society Seattle, United States), 59-68
[34] Cacciagrano, D.; Corradini, F.; Aranda, J.; Valencia, F., Linearity, persistence and testing semantics in the asynchronous pi-calculus, (Amadio, R.; Hildebrandt, T., 14th International Workshop on Expressiveness in Concurrency, EXPRESS’07, Lisbon, Portugal, (2007)), 58-71
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.