The scientific context of the DOTS project is specification, verification and design of information systems. The research domain we have in mind started about 25 years ago with seminal papers by Clarke, Pnueli and Sifakis. Since then the domain has witnessed an impressive growth: a comprehensive theory has been developed, efficient algorithms have been designed, and tools like model checkers have been developed. These tools allow to verify automatically that a model of a system satisfies its specification. The research results have also penetrated the industry world as model checkers are now used in an industrial context for numerous case studies which in turn provided some feedback to improve the theory and algorithms.

Complex systems, such as embedded systems that are widely used nowadays (telecommunication, transport, automation), are often distributed —composed of several components that communicate together—, timed —contain timing constraints—, and open —interact with their environment. Each of these aspects considered separately is now relatively well understood and corresponds to an active research area. The big challenge is to deal with systems which present several of these features.

The aim of the DOTS project is to associate researchers specialized in verification of different aspects mentioned above in order to tackle problems that emerge when considering several features simultaneously. In this way we plan to significantly advance both theory as well as algorithmics of design and verification of distributed, open and timed systems.

The area of formal verification covers now a wide range of problems that share a common theoretical basis, but require specific approaches and techniques. In addition to model checking —the classical problem that consists in deciding whether a given model satisfies a given specification— the DOTS project will mainly address two important verification problems: control and non-interference.

An important characteristic of the DOTS project is our choice of methods and tools to address the problems mentioned above. We plan to use games to cope with interactive aspects and partial orders to deal with the distributed aspect.

More details are available in the full text of the proposal.

Reports

— Biannual activity report —

August 2007: coordinator.
March 2008: coordinator – LSV – LaBRI – IRISA – IRCCyN – LAMSADE.
September 2008: coordinator – LSV – LaBRI – IRISA – IRCCyN – LAMSADE.
March 2009: coordinator – LSV – LaBRI – IRISA – IRCCyN – LAMSADE.

— Deliverables —

Web site. April 2007.

D1.1: Quantitative objectives in timed games. September 2008.
D1.2a: Synthesis of timed controllers. March 2009.
D1.3a: Specification of Timed Non-Interference. March 2008.
D1.3bc: Verification and control for timed non-interference. March 2010.
D2.1: Theory of distributed games. September 2008.
D2.2: Distributed control for restricted specifications. March 2009.
D2.3: Control of asynchronous systems. March 2010.
D2.4b: Quantitative specifications for non-interference. March 2010.
D3.1a: Model for distributed timed systems. September 2008.
D3.1b: Efficient algorithms for distributed timed systems. September 2009.
D3.2: Validation over case studies. September 2009.
D4.1 Specification of realistic DOTS examples. September 2008.

Meetings

Kick-off meeting (Cachan, 12 February 2007).
Meeting on "unfolding of networks of timed automata" (Rennes, 4 April 2007).
Meeting on "Non-interference" (Nantes, 22 May 2007).
Meeting on "Timed games" (Cachan, 18 June 2007).
~~Meeting "DOTS-AVERISS" (Bordeaux, 15-16 November 2007).~~
Meeting on "unfolding" (Rennes, 10 January 2008).
Meeting "AVERISS-DOTS" (Bordeaux, 30-31 January 2008).
Meeting on "Non-interference" (Paris, 15 April 2008).
Meeting on "WP2" (Bordeaux, 15 April 2008).
~~Meeting on "Non-interference" (Nantes, 29 April 2008).~~
Meeting on "Non-interference" (Nantes, 5 June 2008).
Meeting on "unfolding" (Rennes, 3 December 2008).
DOTS meeting (Cachan, 20 January 2009).
Meeting on "Non-interference" (Montréal, 2-6 February 2009).
Meeting on "Non-interference" (Paris, 4 June 2009).
Meeting on case study (Rennes, 3 July 2009).
Meeting on WP2 (Bordeaux, 28-29 October 2009).
DOTS meeting (Nantes, 19 November 2009).
Meeting on "Non-interefernce" (Paris, 7 January 2010).
Meeting on WP2 (Paris, 29 January 2010).
DOTS meeting (Bordeaux, 18 March 2010).

Publications

— 2007 —
	[ABG07]	S. Akshay, Benedikt Bollig and Paul Gastin. Automata and Logics for Timed Message Sequence Charts. In FSTTCS'07, LNCS 4855, p. 290-302. Springer, 2007.
	[AMN07]	S. Akshay, Madhavan Mukund, and K. Narayan Kumar. Checking Coverage for Infinite Collections of Timed Scenarios. In CONCUR'07, LNCS 4703, p. 181-196. Springer, 2007.
	[BCD⁺07]	Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. Uppaal-Tiga: Time for playing games!. In CAV'07, vol. 4590 of LNCS, p. 121-125. Springer, 2007.
	[BGMN07]	Puneet Bhateja, Paul Gastin, Madhavan Mukund and K. Narayan Kumar. Local testing of message sequence charts is difficult. In FCT'07, vol. 4639 of LNCS, p. 76-87. Springer, 2007.
	[BGP07]	Béatrice Bérard, Paul Gastin and Antoine Petit. Timed substitutions for regular signal-event languages. Formal Methods in System Design 31(2), pages 101-134, 2007.
	[BLM07]	Patricia Bouyer, Kim G. Larsen and Nicolas Markey. Model-Checking One-Clock Priced Timed Automata. In FoSSaCS'07, vol. 4423 of LNCS, p. 108-122. Springer, 2007.
	[BLMO07]	Thomas Brihaye, François Laroussinie, Nicolas Markey and Ghassan Oreiby. Timed Concurrent Game Structures. In CONCUR'07, LNCS 4703, p. 445-459. Springer, 2007.
	[BM07]	Patricia Bouyer and Nicolas Markey. Costs are Expensive!. In FORMATS'07, vol. 4763 of LNCS, p. 53-68. Springer, 2007.
	[BMOW07]	Patricia Bouyer, Nicolas Markey, Joël Ouaknine and James B. Worrell. The Cost of Punctuality. In LICS'07, p. 109-118. IEEE Comp. Soc. Press, 2007.
	[BR07]	Marc Boyer and Olivier H. Roux. Comparison of the expressiveness of Arc, Place and Transition Time Petri Nets. In ICATPN'07, vol. 4546 of LNCS, p. 63-82. Springer, 2007.
	[Cas07]	Franck Cassez. Efficient on-the-fly algorithms for partially observable timed games. In FORMATS'07, vol. 4763 of LNCS, p. 5-24. Springer, 2007.
	[CDL⁺07]	Franck Cassez, Alexandre David, Kim G. Larsen, Didier Lime, and Jean-François Raskin. Timed control with observation based and stuttering invariant strategies. In ATVA'07, LNCS 4762, p. 192-206. Springer, 2007.
	[CMR07]	Franck Cassez, John Mullins, and Olivier H. Roux. Synthesis of Non-Interferent Distributed Systems. In MMM-ACNS'07, CCIS 1, p. 307-321. Springer, 2007.
	[CTA07b]	Franck Cassez, Stavros Tripakis, and Karine Altisen. Synthesis of optimal dynamic observers for fault diagnosis of discrete-event systems. In TASE'07, p. 316-325. IEEE Comp. Soc. Press, 2007.
	[EGP07]	Edith Elkind, Blaise Genest, and Doron Peled. Detecting Races in Ensembles of Message Sequence Charts. In TACAS'07, vol. 4424 of LNCS, p. 420-434. Springer, 2007.
	[EGPS07]	Edith Elkind, Blaise Genest, Doron Peled, and Paola Spoletini. Quantifying the Discord: Order Discrepancies in Message Sequence Charts. In ATVA'07, vol. 4762 of LNCS, p. 378-393. Springer, 2007.
	[GGH⁺07]	Thomas Gazagnaire, Blaise Genest, Loïc Hélouët, P.S. Thiagarajan, and Shaofa Yang. Causal High Level Message Sequence Charts. In CONCUR'07, LNCS 4703, p. 166-180. Springer, 2007.
	[GK07]	Paul Gastin and Dietrich Kuske. Uniform satisfiability in PSPACE for local temporal logics over Mazurkiewicz traces. Fundamenta Informaticae 80(1-3), p. 169-197. IOS Press, 2007.
	[GKM07]	Blaise Genest, Dietrich Kuske and Anca Muscholl. On communicating automata with bounded channels. Fundamenta Informaticae 80(1-3), p. 147-167. IOS Press, 2007.
	[HST07]	Frédéric Herbreteau, Grégoire Sutre and The Quang Tran. Unfolding Concurrent Well-Structured Transition Systems. In TACAS'07, vol. 4424 of LNCS, p. 706-720. Springer, 2007.
	[MW07]	Anca Muscholl and Igor Walukiewicz. A lower bound on Web services composition. In FoSSaCS'07, vol. 4423 of LNCS, p. 274-286. Springer, 2007.
— 2008 —
	[ABG⁺08]	S. Akshay, Benedikt Bollig, Paul Gastin, Madhavan Mukund and K. Narayan Kumar. Distributed Timed Automata with Independently Evolving Clocks. In CONCUR'08, vol. 5201 of LNCS, p.~nbsp;82-97. Springer, 2008.
	[BBB⁺08]	Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye and Marcus Größer. Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata. In LICS'08, p. 217-226. IEEE Computer Society Press, 2008.
	[BBJ⁺08]	Patricia Bouyer, Thomas Brihaye, Marcin Jurdzinski, Ranko Lazic, and Michal Rutkowski. Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets. In FORMATS'08, vol. 5215 of LNCS, p. 63-77. Springer, 2008.
	[BCH⁺08]	Béatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, and Olivier H. Roux. When are Timed Automata Weakly Timed Bisimilar to Time Petri Nets?. Theoretical Computer Science 403(2-3):202-220. Esleview, 2008.
	[BCHK08]	Paolo Baldan, Thomas Chatain, Stefan Haar, and Barbara König. Unfolding-based Diagnosis of Systems with an Evolving Topology. In CONCUR'08, vol. 5201 of LNCS, p. 203-217. Springer, 2008.
	[BFL⁺08]	Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey and Jiri Srba. Infinite Runs in Weighted Timed Automata with Energy Constraints. In FORMATS'08, vol. 5215 of LNCS, p. 33-47. Springer, 2008.
	[BGMR08]	Thomas Brihaye, Mohamed Ghannem, Nicolas Markey and Lionel Rieg. Good friends are hard to find!. In TIME'08, p. 32-40. IEEE Computer Society Press, 2008.
	[BHR08]	Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier. Timed Petri nets and timed automata: On the discriminating power of Zeno sequences. In Information and Computation, 206(1):73-107. Elsevier, 2008.
	[BLM08]	Patricia Bouyer, Kim G. Larsen and Nicolas Markey. Model-Checking One-Clock Priced Timed Automata. Logical Methods in Computer Science 4(2:9), 2008.
	[BMOW08]	Patricia Bouyer, Nicolas Markey, Joël Ouaknine and James B. Worrell. On Expressiveness and Complexity in Real-time Model Checking. In ICALP'08, vol. 5126 of LNCS, p. 124-135. Springer, 2008.
	[BMR08]	Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier. Robust Analysis of Timed Automata via Channel Machines. In FoSSaCS'08, vol. 4962 of LNCS, p. 157-171. Springer, 2008.
	[DDMR08]	Martin De Wulf, Laurent Doyen, Nicolas Markey and Jean-François Raskin. Robust Safety of Timed Automata. Formal Methods in System Design 33(1-3):45-84. Springer, 2008.
	[DGH08]	Philippe Darondeau, Blaise Genest, and Loïc Hélouet. Products of Message Sequence Charts. In FOSSACS'08, vol. 4962 of LNCS, p. 459-474. Springer, 2008.
	[DGTY08]	Philippe Darondeau, Blaise Genest, P.S. Thiagarajan, and Shaofa Yang. Quasi-Static Scheduling of Communicating Tasks. In CONCUR'08, vol. 5201 of LNCS, p. 310-324. Springer, 2008.
	[GM08]	Blaise Genest, Anca Muscholl. Pattern Matching and Membership for Hierarchical Message Sequence Charts. Theory of Computing Systems 42(4):536-567. Springer, 2008.
— 2009 —
	[ACEF09]	Étienne André, Thomas Chatain, Emmanuelle Encrenaz, and Laurent Fribourg. An Inverse Method for Parametric Timed Automata. International Journal of Foundations of Computer Science 20(5):819-836, 2009.
	[BCDL09]	Peter Bulychev, Thomas Chatain, Alexandre David, and Kim G. Larsen. Checking simulation relation between timed game automata. In FORMATS'09, vol. 5813 of LNCS, p. 73-87. Springer, 2009.
	[BDLM09]	Thomas Brihaye, Arnaud Da Costa, François Laroussinie, and Nicolas Markey. ATL with Strategy Contexts and Bounded Memory. In LFCS'09, vol. 5407 of LNCS, p. 92-106. Springer, 2009.
	[BDMR09]	Patricia Bouyer, Marie Duflot, Nicolas Markey, and Gabriel Renault. Measuring Permissivity in Finite Games. In CONCUR'09, vol 5710 of LNCS, p. 196-210. Springer, 2009.
	[BF09]	Patricia Bouyer and Vojtech Forejt. Reachability in Stochastic Timed Games. In ICALP'09, vol 5556 of LNCS, p. 103-114. Springer, 2009.
	[BGG09]	Nathalie Bertrand, Blaise Genest and Hugo Gimbert. Qualitative Determinacy and Decidability of Stochastic Games with Signals. In LICS'09, p. 309-318, IEEE COmputer Society Press, 2009.
	[BGH09]	Benedikt Bollig, Manuela-Lidia Grindei, and Peter Habermehl. Realizability of Concurrent Recursive Programs. In FoSSaCS'09, vol. 5504 of LNCS, p. 410-424. Springer, 2009.
	[BH09]	Béatrice Bérard and Serge Haddad. Interrupt Timed Automata. In FoSSaCS'09, vol 5504 of LNCS, p. 410-424. Springer, 2009.
	[BHR09]	Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier. Undecidability Results for Timed Automata with Silent Transitions. Fundamenta Informaticae 92(1-2):1-25. IOS Press, 2009.
	[BRBH09]	Anne Bouillard, Sidney Rosario, Albert Benveniste, and Stefan Haar. Monotonicity in Service Orchestrations. In ICATPN'09, vol. 5606 of LNCS, p. 263-282. Springer, 2009.
	[CDL09]	Thomas Chatain, Alexandre David, and Kim G. Larsen. Playing Games with Timed Games. In ADHS'09, 2009.
	[CGS09]	Thomas Chatain, Paul Gastin, and Nathalie Sznajder. Natural Specifications Yield Decidability for Distributed Synthesis of Asynchronous Systems. In SOFSEM'09, vol. 5404 of LNCS, p. 141-152. Springer, 2009.
	[CM09]	Franck Cassez and Nicolas Markey. Control of Timed Systems. In Communicating Embedded Systems - Software and Design, chap. 3. Wiley-ISTE, 2009.
	[DG09]	Volker Diekert and Paul Gastin. Local safety and local liveness for distributed systems. In Perspectives in Concurrency Theory, p. 86-106. Universities Press, 2009.
	[GH09]	Hugo Gimbert and Florian Horn. Solving Simple Stochastic Games with Few Random Vertices. Logical Methods in Computer Science 5(2), 2009.
	[GMN09]	Paul Gastin, Madhavan Mukund, and K. Narayan Kumar. Reachability and boundedness in time-constrained MSC graphs. In Perspectives in Concurrency Theory, p. 157-183. Universities Press, 2009.
	[GSZ09]	Paul Gastin, Nathalie Sznajder, and Marc Zeitoun. Distributed synthesis for well-connected architectures. Formal Methods in System Design 34(3):215-237. Springer, 2009.
	[JR09]	Claude Jard and Olivier H. Roux (eds). Communicating Embedded Systems – Software and design. Wiley-ISTE, 2009.
	[RS09]	Pierre-Alain Reynier and Arnaud Sangnier. Weak Time Petri Nets strike back!. In CONCUR'09, vol. 5710 of LNCS, pages 557-571. Springer, 2009.
— 2010 —
	[BCHK10]	Paolo Baldan, Thomas Chatain, Stefan Haar, and Barbara König. Unfolding-based Diagnosis of Systems with an Evolving Topology. Information and Computation. Elsevier, 2010. To appear.
	[BCL10]	Patricia Bouyer, Franck Cassez, and François Laroussinie. Timed Modal Logics for Real-Time Systems: Specification, Verification and Control. Journal of Logic, Language and Information, 2010. To appear.
	[BCM10]	Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the Expressiveness of TPTL and MTL. Information and Computation 208(2):97-116. Elsevier, 2010.
	[BEGP09]	Dragan Bosnacki, Edith Elkind, Blaise Genest, and Doron Peled. On Commutativity Based Edge Lean Search. Annals Math & AI 56(2):187-210. Springer, 2009.
	[BFLM10]	Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, and Nicolas Markey. Timed Automata with Observers under Energy Constraints. In HSCC'10. ACM Press, 2010. To appear.
	[BH10]	Benedikt Bollig and Loïc Hélouët. Realizability of Dynamic MSC Languages. In CSR'10, LNCS. Springer, 2010. To appear.
	[CF10]	Thomas Chatain and Éric Fabre. Factorization Properties of Symbolic Unfoldings of Colored Petri Nets. In ICATPN'10, LNCS. Springer, 2010. To appear.
	[CJ10]	Thomas Chatain and Claude Jard. Sémantique concurrente symbolique des réseaux de Petri saufs et dépliages finis des réseaux temporels. In NOTERE'10. IEEE Computer Society Press, 2010. To appear.
	[DGTY10]	Philippe Darondeau, Blaise Genest, P.S. Thiagarajan, and Shaofa Yang. Quasi-Static Scheduling of Communicating Tasks. Information and Computation. Elsevier, 2010. To appear.
	[EGPS10]	Edith Elkind, Blaise Genest, Doron Peled, and Paola Spoletini. Quantifying the Discord: Order Discrepancies in Message Sequence Charts. International Journal of Foundations of Computer Science 21(2):211-233. WorldSciNet, 2010.
	[GGHTY09]	Thomas Gazagnaire, Blaise Genest, Loïc Hélouet, P.S. Thiagarajan, and Shaofa Yang. Causal Message Sequence Charts. Theoretical Computer Science 410(41): 4094-4110, Elsevier, 2009.
	[GGMW10]	Blaise Genest, Hugo Gimbert, Anca Muscholl, and Igor Walukiewicz. Optimal Zielonka-Type Construction of Deterministic Asynchronous Automata. In ICALP'10, LNCS. Springer, 2010. To appear.
	[GH10]	Hugo Gimbert and Florian Horn. Solving Simple Stochastic Tail Games. In SODA'10, p. 847-862. SIAM, 2010.
	[GK10]	Paul Gastin and Dietrich Kuske. Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces. Information and Computation. Elsevier, 2010. To appear.
	[HLMS10]	Alexander Heussner, Jerome Leroux, Anca Muscholl, and Gregoire Sutre. Reachability Analysis of Communicating Networks with Pushdowns. In FOSSACS'10, vol. 6014 of LNCS. Springer, 2010.
	[HSW10]	Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Efficient Emptyness Check for Timed Büchi Automata. In CAV'10, LNCS. Springer, 2010.