@ARTICLE{DL06:MLTS,
  title = {{Multi Labelled Transition Systems for Nominal Calculi and their Logics}},
  author = {{Rocco} {De Nicola} and {Michele} {Loreti}},
  journal = {Mathematical Structures in Computer Science},
  pages = {107-143},
  abstract = {Action Labelled transition systems (LTS) have proved to be a fundamental model for describing and proving properties of concurrent systems. In this paper, we introduce Multiple Labelled Transition Systems (MLTS) as generalizations of LTS that permit also dealing with systems features that are becoming more and more important when considering languages and models for network aware programming. MLTS permit describing not only the actions systems can perform but also their usage of resources and their handling (creation, revelation...) of names; these are essential to model changing evaluation environments. We also introduce MoMo, a logic inspired by Hennessy-Milner Logic and the mu-calculus, that permits also considering state properties in a distributed environment and the impact of actions and movements over the different sites. MoMo operators are interpreted over MLTS and both MLTS and MoMo are used to provide a semantic framework to describe two basic calculi for mobile computing, namely KKlaim and the asynchronous pi-calculus},
  volume = {18},
  number = {1},
  year = {2008},
  url = {http://rap.dsi.unifi.it/sensoriasite/2006-DNL.pdf},
  partner = {DSIUF},
  task = {T3.2},
}