Choreographic Autonomous Systems

A swarm of drones, a team of robots, a federation of microservices: when many autonomous components must cooperate, getting the interaction right is the hard part. Deadlocks, races and protocol violations are notoriously difficult to find by testing alone.

In the Choreographic Autonomous Systems area we take a correct-by-construction approach. In a choreography the global interaction is written once, from the point of view of the whole system. Executable code for each participant is then derived automatically, and is guaranteed to follow the protocol.

We build on a long tradition of the lab in formal models of distributed systems (process calculi, bigraphs, coalgebras, type theory) and turn these foundations into languages and tools for real autonomous systems.

Publications

1. Attribute-based memory updates with priorities for collective adaptive systems

   Michele Pasqua, Marino Miculan

   International Journal on Software Tools for Technology Transfer · 2026

   Journal articleChoreographiesDOI PDF

   BibTeX

   Copy

   @Article{PM:sttt26,
     groups = {choreographies},
     author    = {Pasqua, Michele and Miculan, Marino},
     title     = {Attribute-based memory updates with priorities for collective adaptive systems},
     journal   = {International Journal on Software Tools for Technology Transfer},
     year      = {2026},
     doi       = {10.1007/s10009-026-00856-y},
     html      = {https://doi.org/10.1007/s10009-026-00856-y},
     pdf = "https://rdcu.be/fdYwk"
   }

2. KLAIM, Certified: Mechanising Flow Logic for Tuple-Space Coordination

   Marino Miculan

   Journal of Logical and Algebraic Methods in Programming, pp. 101179 · 2026

   Journal articleChoreographiesDOI Code

   BibTeX

   Copy

   @Article{m:jlamp26,
     groups = {choreographies},
   	author    = {Miculan, Marino},
   	title     = {{KLAIM}, Certified: Mechanising Flow Logic for Tuple-Space Coordination},
   	journal   = {Journal of Logical and Algebraic Methods in Programming},
   	year      = {2026},
   	pages     = {101179},
   	doi       = {10.1016/j.jlamp.2026.101179},
   	html      = {https://doi.org/10.1016/j.jlamp.2026.101179},
   	code      = {https://zenodo.org/records/22171485},
   	issn      = {2352-2208},
     selected  = true,
   }

3. Reliable Decision Loops in Socio-Technical Collective Adaptive Systems

   Marino Miculan

   Proc. ISoLA 2026, Lecture Notes in Computer Science 17141 · Springer · 2026

   Conference paperTo appearChoreographiesDOI

   BibTeX

   Copy

   @InProceedings{m:isola26,
     groups = {choreographies},
   	author    = {Miculan, Marino},
   	editor    = {Margaria, Tiziana and Steffen, Bernhard},
   	title     = {Reliable Decision Loops in Socio-Technical Collective Adaptive Systems},
   	booktitle = {Proc. ISoLA 2026},
   	series    = {Lecture Notes in Computer Science},
   	volume    = {17141},
   	publisher = {Springer},
   	year      = {2026},
   	doi       = {10.1007/978-3-032-40108-3_5},
   	note      = {To appear}
   }

4. Attribute-Based Communication over Pub/Sub: Transactional Coordination for Smart Systems

   Marco Comini, Luca Gemolotto, Marino Miculan

   45th IFIP International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2025, Lecture Notes in Computer Science 15732, pp. 96–113 · Springer · 2025

   Conference paperChoreographiesDOI

   BibTeX

   Copy

   @InProceedings{cgm:forte25,
     groups = {choreographies},
   author="Comini, Marco and Gemolotto, Luca and Miculan, Marino",
   editor="Ferreira, Carla and Mezzina, Claudio Antares",
   title="Attribute-Based Communication over Pub/Sub: Transactional Coordination for Smart Systems",
   booktitle="45th IFIP International Conference on Formal Techniques for Distributed Objects, Components, and Systems, {FORTE 2025}",
   year="2025",
   series="Lecture Notes in Computer Science",
   volume="15732",
   publisher="Springer",
   pages="96--113",
   doi="10.1007/978-3-031-95497-9_6",
   html="https://link.springer.com/chapter/10.1007/978-3-031-95497-9_6",
   isbn="978-3-031-95497-9"
   }

5. Behavioral equivalences for AbU: Verifying security and safety in distributed IoT systems

   Michele Pasqua, Marino Miculan

   Theoretical Computer Science 998, pp. 114537 · 2024

   Journal articleSecurityChoreographiesDOI Link

   BibTeX

   Copy

   @article{PASQUA2024114537,
     groups = {cybersecurity, choreographies},
   title = {Behavioral equivalences for {AbU}: Verifying security and safety in distributed IoT systems},
   journal = {Theoretical Computer Science},
   volume = {998},
   pages = {114537},
   year = {2024},
   issn = {0304-3975},
   doi = {10.1016/j.tcs.2024.114537},
   html = {https://www.sciencedirect.com/science/article/pii/S030439752400152X},
   author = {Michele Pasqua and Marino Miculan},
   keywords = {ECA rules, IoT programming, Distributed systems, Bisimulations, Formal methods, Autonomic computing, Verification},
   selected=false
   }

6. Local Reasoning and Attribute-Based Memory Updates for Enforcing Global Invariants in Collective Adaptive Systems

   Michele Pasqua, Marino Miculan

   12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024, pp. 351–367 · Springer · 2024

   Conference paperChoreographiesDOI PDF

   BibTeX

   Copy

   @InProceedings{pm:isola24,
     groups = {choreographies},
   author="Pasqua, Michele and Miculan, Marino",
   editor="Margaria, Tiziana and Steffen, Bernhard",
   title="Local Reasoning and Attribute-Based Memory Updates for Enforcing Global Invariants in Collective Adaptive Systems",
   booktitle="12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2024",
   year="2024",
   publisher="Springer",
   pages="351--367",
   isbn="978-3-031-75107-3",
   doi="10.1007/978-3-031-75107-3_21",
   html="https://doi.org/10.1007/978-3-031-75107-3_21",
   pdf="https://marino.miculan.org/assets/pdf/2024-ISOLA.pdf"
   }

7. AbU: A calculus for distributed event-driven programming with attribute-based interaction

   Michele Pasqua, Marino Miculan

   Theoretical Computer Science 958, pp. 113841 · 2023

   Journal articleChoreographiesDOI Link

   BibTeX

   Copy

   @article{PASQUA2023113841,
     groups = {choreographies},
   title = {{AbU}: A calculus for distributed event-driven programming with attribute-based interaction},
   journal = {Theoretical Computer Science},
   volume = 958,
   pages = {113841},
   year = 2023,
   issn = {0304-3975},
   doi = {10.1016/j.tcs.2023.113841},
   html = {https://www.sciencedirect.com/science/article/pii/S0304397523001548},
   author = {Michele Pasqua and Marino Miculan},
   selected = true,
   keywords = {ECA rules, Attribute-based communication, Distributed systems, Formal methods, Edge computing, IoT programming},
   }

8. Composable partial multiparty session types for open systems

   Claude Stolze, Marino Miculan, Pietro Di Gianantonio

   Software and Systems Modeling, pp. 473-494 · 2023

   Journal articleChoreographiesDOI

   BibTeX

   Copy

   @article{stolze2022composable,
     groups = {choreographies},
     title={Composable partial multiparty session types for open systems},
     author={Stolze, Claude and Miculan, Marino and Di Gianantonio, Pietro},
     journal={Software and Systems Modeling},
     year=2023,
     html= {https://doi.org/10.1007/s10270-022-01040-x},
     doi = {10.1007/s10270-022-01040-x},
     publisher={Springer},
     pages = {473-494},
     number=22,
     keywords={concurrency,session types,process calculi,compositionality}
   }

9. DBCChecker: a Bigraph-based Tool for Checking Security Properties of Container Compositions

   Andrea Altarui, Marino Miculan, Matteo Paier

   Proceedings of the Italian Conference on Cyber Security (ITASEC 2023), Bari, Italy, May 2-5, 2023, CEUR Workshop Proceedings 3488 · CEUR-WS.org · 2023

   Conference paperSecurityChoreographies PDF

   BibTeX

   Copy

   @inproceedings{DBLP:conf/itasec/AltaruiMP23,
     groups = {cybersecurity, choreographies},
     author       = {Andrea Altarui and
                     Marino Miculan and
                     Matteo Paier},
     editor       = {Francesco Buccafurri and
                     Elena Ferrari and
                     Gianluca Lax},
     title        = {{DBCChecker}: a Bigraph-based Tool for Checking Security Properties
                     of Container Compositions},
     booktitle    = {Proceedings of the Italian Conference on Cyber Security ({ITASEC}
                     2023), Bari, Italy, May 2-5, 2023},
     series       = {{CEUR} Workshop Proceedings},
     volume       = {3488},
     publisher    = {CEUR-WS.org},
     year         = {2023},
     pdf          = {https://ceur-ws.org/Vol-3488/paper01.pdf},
     html    = {https://ceur-ws.org/Vol-3488}
   }

10. A Calculus for Subjective Communication

    Marino Miculan, Matteo Paier

    Proceedings of the 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022, Rome, Italy, September 7-9, 2022, CEUR Workshop Proceedings 3284, pp. 148–160 · CEUR-WS.org · 2022

    Conference paperChoreographies PDF

    BibTeX

    Copy

    @inproceedings{DBLP:conf/ictcs/MiculanP22,
    groups = {choreographies},
    author = {Marino Miculan and
    Matteo Paier},
    editor = {Dal Lago, Ugo and
    Daniele Gorla},
    title = {A Calculus for Subjective Communication},
    booktitle = {Proceedings of the 23rd Italian Conference on Theoretical Computer
    Science, {ICTCS} 2022, Rome, Italy, September 7-9, 2022},
    series = {{CEUR} Workshop Proceedings},
    volume = {3284},
    pages = {148--160},
    publisher = {CEUR-WS.org},
    year = {2022},
    pdf = {http://ceur-ws.org/Vol-3284/1841.pdf}
    }

All publications in this area