×

zbMATH — the first resource for mathematics

Multiple-labelled transition systems for nominal calculi and their logics. (English) Zbl 1141.68047
Summary: Action-Labelled Transition Systems (LTSs) have proved to be a fundamental model for describing and proving properties of concurrent systems. In this paper we introduce Multiple-Labelled Transition Systems (MLTSs) as generalisations of LTSs that enable us to deal with system features that are becoming increasingly important when considering languages and models for network-aware programming. MLTSs enable us to describe not only the actions that systems can perform but also their usage of resources and their handling (creation, revelation, …) of names; these are essential for modelling changing evaluation environments. We also introduce MoMo, which is a logic inspired by Hennessy-Milner Logic and the \(\mu \)-calculus, that enables us to consider state properties in a distributed environment and the impact of actions and movements over the different sites. MoMo operators are interpreted over MLTSs and both MLTSs and MoMo are used to provide a semantic framework to describe two basic calculi for mobile computing, namely \(\mu\) Klaim and the asynchronous \(\pi \)-calculus.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B70 Logic in computer science
Software:
MoMo
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] DOI: 10.1006/inco.2001.3089 · Zbl 1009.68081
[2] Honda, Springer-Verlag Lecture Notes in Computer Science 512 pp 133– (1991)
[3] Gelernter, Springer-Verlag Lecture Notes in Computer Science 366 pp 20– (1989)
[4] DOI: 10.1145/2363.2433 · Zbl 0559.68030
[5] DOI: 10.1016/j.ic.2004.11.005 · Zbl 1101.68060
[6] Fournet, Springer-Verlag Lecture Notes in Computer Science 1119 pp 406– (1996)
[7] DOI: 10.1145/63334.63337
[8] DOI: 10.1023/A:1014530313153 · Zbl 1034.68600
[9] De Nicola, Springer-Verlag Lecture Notes in Computer Science 3657 pp 95– (2005)
[10] DOI: 10.1016/S0304-3975(99)00231-5 · Zbl 0954.68108
[11] DOI: 10.1109/32.685256
[12] Caires, Springer-Verlag Lecture Notes in Computer Science 2987 pp 72– (2004)
[13] DOI: 10.1006/inco.1996.0072 · Zbl 0864.68036
[14] Boreale, Springer-Verlag Lecture Notes in Computer Science 4184 pp 38– (2006)
[15] Bettini, Springer-Verlag Lecture Notes in Computer Science 2874 pp 88– (2003)
[16] DOI: 10.1016/S0304-3975(97)00223-5 · Zbl 0915.68009
[17] DOI: 10.1016/0304-3975(93)90156-N · Zbl 0778.68033
[18] DOI: 10.1109/32.666824 · Zbl 05113387
[19] DOI: 10.1145/2455.2460 · Zbl 0629.68021
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.