, Patterns Project, 1999.

, Patterns Project: List of specifications, 1999.

G. S. Avrunin, J. C. Corbett, M. B. Dwyer, C. S. Pasareanu, and S. F. Siegel, Comparing Finite-State Verification Techniques for Concurrent Software, 1999.

E. Bartocci, Sampling-based Decentralized Monitoring for Networked Embedded Systems, Proceedings Third International Workshop on Hybrid Autonomous Systems, HAS 2013, vol.124, pp.85-99, 2013.

, Lectures on Runtime Verification -Introductory and Advanced Topics, Lecture Notes in Computer Science, vol.10457, 2018.

E. Bartocci, Y. Falcone, B. Bonakdarpour, C. Colombo, N. Decker et al., First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014, International Journal on Software Tools for Technology Transfer, pp.1-40, 2017.
URL : https://hal.archives-ouvertes.fr/cea-01845191

D. A. Basin, F. Klaedtke, and E. Zalinescu, Failure-aware Runtime Verification of Distributed Systems, 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, vol.45, pp.590-603, 2015.

A. Bauer and Y. Falcone, Decentralised LTL monitoring, Formal Methods in System Design, vol.48, pp.46-93, 2016.
URL : https://hal.archives-ouvertes.fr/hal-00857286

A. Bauer, M. Leucker, and C. Schallhart, Runtime Verification for LTL and TLTL, ACM Trans. Softw. Eng. Methodol, vol.20, p.14, 2011.

A. K. Bauer and Y. Falcone, Decentralised LTL Monitoring, FM 2012: Formal Methods -18th International Symposium, vol.7436, pp.85-100, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00857286

B. Bonakdarpour, P. Fraigniaud, S. Rajsbaum, and C. Travers, Challenges in Fault-Tolerant Distributed Runtime Verification, pp.363-370, 2016.

D. Buchfuhrer, C. Umans, ;. , L. Aceto, and I. Damgård, The Complexity of Boolean Formula Minimization, Proceedings, Part I: Tack A: Algorithms, Automata, Complexity, and Games (Lecture Notes in Computer Science), vol.5125, pp.24-35, 2008.

C. Colombo and Y. Falcone, Organising LTL Monitors over Distributed Systems with a Global Clock, Runtime Verification -5th International Conference, vol.8734, pp.140-155, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01120551

C. Colombo and Y. Falcone, Organising LTL monitors over distributed systems with a global clock, Formal Methods in System Design, vol.49, pp.109-158, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01120551

S. Sylvain-cotard, J. Faucou, A. Béchennec, Y. Queudet, and . Trinquet, A Data Flow Monitoring Service Based on Runtime Verification for AUTOSAR, 14th IEEE International Conference on High Performance Computing and Communication & 9th IEEE International Conference on Embedded Software and Systems, HPCC-ICESS 2012, pp.1508-1515, 2012.

D. Ben, S. Angelo, C. Sankaranarayanan, W. Sánchez, B. Robinson et al., LOLA: Runtime Monitoring of Synchronous Systems, 12th International Symposium on Temporal Representation and Reasoning (TIME 2005, pp.166-174, 2005.

N. Decker, P. Gottschling, C. Hochberger, M. Leucker, T. Scheffel et al., Rapidly Adjustable Non-intrusive Online Monitoring for Multi-core Systems, Formal Methods: Foundations and, pp.179-196, 2017.

V. Diekert and M. Leucker, Topology, monitorable properties and runtime verification, Theoretical Aspects of Computing, vol.537, pp.29-41, 2014.

V. Diekert and A. Muscholl, On Distributed Monitoring of Asynchronous Systems, Logic, Language, Information and Computation -19th International Workshop, vol.7456, pp.70-84, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00825771

A. Duret-lutz, Manipulating LTL formulas using Spot 1.0, Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13), vol.8172, pp.442-445, 2013.

M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, Patterns in Property Specifications for Finite-State Verification, Proceedings of the 1999 International Conference on Software Engineering, ICSE' 99, pp.411-420, 1999.

A. El, -. Hokayem, and Y. Falcone, Monitoring Decentralized Specifications, Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp.125-135, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01653725

A. El, -. Hokayem, and Y. Falcone, THEMIS: A Tool for Decentralized Monitoring Algorithms, Proceedings of 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA'17-DEMOS), 2017.
URL : https://hal.archives-ouvertes.fr/hal-01653727

A. El, -. Hokayem, Y. Falcone, and . Themis-website, , 2017.

A. El, -. Hokayem, and Y. Falcone, THEMIS Article Artifact, 2018.

Y. Falcone, You Should Better Enforce Than Verify, Runtime Verification -First International Conference, RV 2010, St. Julians, Malta, vol.6418, pp.89-105, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00523653

Y. Falcone, T. Cornebize, and J. Fernandez, Efficient and Generalized Decentralized Monitoring of Regular Languages, Formal Techniques for Distributed Objects, Components, and Systems -34th IFIP WG 6.1 International Conference, FORTE 2014, Held as Part of the 9th International Federated Conference on Distributed Computing Techniques, vol.8461, pp.66-83, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00972559

Y. Falcone, J. Fernandez, and L. Mounier, What can you verify and enforce at runtime? STTT, vol.14, pp.349-382, 2012.

Y. Falcone, K. Havelund, and G. Reger, NATO science for peace and security series, d: information and communication security, Engineering Dependable Software Systems, vol.34, pp.141-175, 2013.

Y. Falcone, S. Krstic, G. Reger, and D. Traytel, A Taxonomy for Classifying Runtime Verification Tools, Runtime Verification -18th International Conference, vol.11237, pp.241-262, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01882410

Y. Falcone, L. Mariani, A. Rollet, and S. Saha, Runtime Failure Prevention and Reaction, pp.103-134, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01723606

A. Francalanza, J. A. Pérez, and C. Sánchez, Runtime Verification for Decentralised and Distributed Systems, pp.176-210, 2018.

. Sylvain-hallé, When RV Meets CEP, pp.68-91, 2016.

S. Hallé, R. Khoury, and S. Gaboury, Event Stream Processing with Multiple Threads, pp.359-369, 2017.

G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm et al., An Overview of AspectJ, ECOOP 2001 -Object-Oriented Programming, 15th European Conference, vol.2072, pp.327-353, 2001.

M. Kim, M. Viswanathan, H. Ben-abdallah, S. Kannan, I. Lee et al., Formally specified monitoring of temporal properties, 11th Euromicro Conference on Real-Time Systems (ECRTS 1999, pp.114-122, 1999.

M. Leucker and C. Schallhart, A brief account of runtime verification, J. Log. Algebr. Program, vol.78, pp.293-303, 2009.

M. Leucker, M. Schmitz, and D. Tellinghusen, Runtime Verification for Interconnected Medical Devices, pp.380-387, 2016.

, Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications -7th International Symposium, vol.9953, 2016.

M. Mostafa and B. Bonakdarpour, Decentralized Runtime Verification of LTL Specifications in Distributed Systems, 2015 IEEE International Parallel and Distributed Processing Symposium, IPDPS 2015, pp.494-503, 2015.

A. Natarajan, H. Chauhan, N. Mittal, and V. K. Garg, Efficient abstraction algorithms for predicate detection, Theor. Comput. Sci, vol.688, pp.24-48, 2017.

A. Vinit, V. K. Ogale, and . Garg, Detecting Temporal Logic Predicates on Distributed Computations, DISC 2007, Proceedings (Lecture Notes in Computer Science), Andrzej Pelc, vol.4731, pp.420-434, 2007.

A. Pnueli and A. Zaks, PSL Model Checking and Run-Time Verification Via Testers, FM 2006: Formal Methods, 14th International Symposium on Formal Methods, vol.4085, pp.573-586, 2006.

G. Rosu and K. Havelund, Rewriting-Based Techniques for Runtime Verification, Autom. Softw. Eng, vol.12, pp.151-197, 2005.

T. Scheffel and M. Schmitz, Three-valued asynchronous distributed runtime verification, Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, pp.52-61, 2014.

K. Sen, A. Vardhan, G. Agha, and G. Rosu, Efficient Decentralized Monitoring of Safety in Distributed Systems, 26th International Conference on Software Engineering, pp.418-427, 2004.

M. Shapiro, M. Nuno, C. Preguiça, M. Baquero, and . Zawirski, Conflict-Free Replicated Data Types, Stabilization, Safety, and Security of Distributed Systems -13th International Symposium, vol.6976, pp.386-400, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00609399

. Robert-endre-tarjan, Depth-First Search and Linear Graph Algorithms, SIAM J. Comput, vol.1, pp.146-160, 1972.

, The Chiron Team. Chiron User Interface, 1999.

P. Thati and G. Rosu, Monitoring Algorithms for Metric Temporal Logic Specifications, Electronic Notes in Theoretical Computer Science, vol.113, pp.145-162, 2005.

L. G. Valiant, A Bridging Model for Parallel Computation, Commun. ACM, vol.33, pp.103-111, 1990.

T. J. Gene, A. J. Wuu, and . Bernstein, Efficient Solutions to the Replicated Log and Dictionary Problems, Operating Systems Review, vol.20, pp.57-66, 1986.

, We note that, since the automaton is deterministic, there is a unique q i+1 such that q i+1 = ?(q i , evt i+1 )

E. Choreography, In this section, we present the setup phase. As such, we present the generation of the decentralized specification from a start LTL formula. Choreography begins by taking the main formula, then deciding to split it into subformulas. Each monitor will monitor the subformula, notify other monitors of its verdict, and when needed respawn . Recall from the definition of ? ? (see Definition 5.4), that monitoring is recursively applied to the remainder of a trace starting at the current event. That is

, ? A id the automaton that monitors the subformula

I. ?-ref, Mons the monitors that this monitor should notify of a verdict

I. ?-coref, Mons the monitors that send their verdicts to this monitor