Formal Modeling and Analysis of Timed Systems : 15th International Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings / edited by Alessandro Abate, Gilles Geeraerts.

This book constitutes the refereed proceedings of the 15th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2017, held in Berlin, Germany, in September 2017. The aim of FORMATS is to promote the study of fundamental and practical aspects of timed systems, and to bring together researchers from different disciplines that share interests in modelling and analysis of timed systems and, as a generalization, hybrid systems.

Intro -- Preface -- Organization -- Contents -- Invited Talk -- Euler's Method Applied to the Control of Switched Systems -- 1 Introduction -- 2 Switched Systems and (R, S)-Stability -- 2.1 Switched Systems -- 2.2 (R, S)-Stability -- 2.3 Guaranteed Integration -- 3 Euler's Method and Error Estimation -- 3.1 One-Sided Lipschitz Constant -- 3.2 Euler Approximate Solutions -- 3.3 Application to Control Synthesis for (R, S)-Stability -- 3.4 Avoiding Wrapping Effect with Euler's Method -- 3.5 Numerical Results -- 4 ODEs with Uncertainty -- 4.1 Bounded Uncertainty

4.2 Application to Distributed Control Synthesis -- 5 Final Remarks -- References -- Timed Models -- On the Determinization of Timed Systems -- 1 Introduction -- 2 Definitions -- 2.1 Timed Domains -- 2.2 Updates -- 2.3 Automata over Timed Domains -- 2.4 Finite Representation of Automata over Timed Domains -- 2.5 Commands -- 2.6 Different Notions of Determinism -- 3 Determinization of ATD -- 3.1 Full-Command Determinization -- 3.2 Timed-Command Determinization -- 4 Applications -- 4.1 Applications to Plain Timed Automata -- 4.2 Applications to Event-Clock Automata

4.3 Application to Perturbed Timed Automata -- 5 Conclusions and Future Work -- References -- On Global Scheduling Independency in Networks of Timed Automata -- 1 Introduction -- 2 Preliminaries -- 3 Non-blocking Operational Semantics -- 4 Deciding Independency from Global Scheduling -- 5 Evaluation -- 6 Conclusion -- References -- Optimal Reachability in Cost Time Petri Nets -- 1 Introduction -- 1.1 Related Works -- 1.2 Our Contribution -- 2 Cost Time Petri Nets -- 2.1 Preliminaries -- 2.2 Time Petri Nets -- 2.3 Cost Time Petri Nets -- 3 Cost State Classes -- 4 Symbolic Algorithm

5 Computing the Simple Cost State Classes -- 6 Termination of the Algorithm -- 7 Practical Results -- 7.1 EPOC (Energy Proportional and Opportunistic Computing systems) -- 8 Conclusion -- References -- Hybrid Systems -- Optimal Control for Multi-mode Systems with Discrete Costs -- 1 Introduction -- 2 Preliminaries -- 2.1 Formal Definition of Multi-mode Systems -- 2.2 Schedules, Their Cost and Safety -- 2.3 Structure of Optimal Schedules -- 2.4 Approximation Algorithms -- 3 Complexity of Limit-Safe and -safe Finite Control -- 4 Structure of Finite Control in One-Dimension

5 Complexity of Optimal Control in One-Dimension -- 5.1 Infinite Time Horizon -- 5.2 Finite Time Horizon -- 6 Approximate Optimal Control in One-Dimension -- References -- Augmented Complex Zonotopes for Computing Invariants of Affine Hybrid Systems -- 1 Introduction -- 2 Hybrid Systems and Positive Invariants -- 3 Augmented Complex Zonotopes -- 4 Computation of Positive Invariants -- 5 Experiments -- 6 Conclusion -- References -- Conic Abstractions for Hybrid Systems -- 1 Introduction -- 2 Preliminaries -- 3 Conic Abstractions of Affine Systems