Formal modeling and analysis of timed systems : 16th international conference, FORMATS 2018, Beijing, China, September 4-6, 2018 : proceedings

This book constitutes the refereed proceedings of the 16th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2018, held in Beijing, China, in September 2018. The 14 papers presented in this volume were carefully reviewed and selected from 29 submissions. The papers are organized in the following topical sections: invited papers, temporal logics, distributed timed systems, behavioral equivalences, timed words, and continuous dynamical systems. 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 modeling and analysis of timed systems and, as a generalization, hybrid systems. Front Matter ....Pages I-X Front Matter ....Pages 1-1 Stochastic Temporal Logic Abstractions: Challenges and Opportunities (Jyotirmoy V. Deshmukh, Panagiotis Kyriakis, Paul Bogdan)....Pages 3-16 Models of Timed Systems (Edward A. Lee)....Pages 17-33 Front Matter ....Pages 35-35 TCTL Model Checking Lower/Upper-Bound Parametric Timed Automata Without Invariants (Étienne André, Didier Lime, Mathias Ramparison)....Pages 37-52 Monitoring Temporal Logic with Clock Variables (Adrián Elgyütt, Thomas Ferrère, Thomas A. Henzinger)....Pages 53-70 Reactive Synthesis for Robotic Swarms (Salar Moarref, Hadas Kress-Gazit)....Pages 71-87 Front Matter ....Pages 89-89 Perfect Timed Communication Is Hard (Parosh Aziz Abdulla, Mohamed Faouzi Atig, Shankara Narayanan Krishna)....Pages 91-107 On Persistency in Time Petri Nets (Kamel Barkaoui, Hanifa Boucheneb)....Pages 108-124 A Relational Model for Probabilistic Connectors Based on Timed Data Distribution Streams (Meng Sun, Xiyue Zhang)....Pages 125-141 Front Matter ....Pages 143-143 Weighted Branching Systems: Behavioural Equivalence, Behavioural Distance, and Their Logical Characterisations (Mathias Claus Jensen, Kim Guldstrand Larsen, Radu Mardare)....Pages 145-161 Trace Relations and Logical Preservation for Markov Automata (Arpit Sharma)....Pages 162-178 Non-bisimulation Based Behavioral Relations for Markov Automata (Arpit Sharma)....Pages 179-196 Front Matter ....Pages 197-197 Distance on Timed Words and Applications (Eugene Asarin, Nicolas Basset, Aldric Degorre)....Pages 199-214 Online Timed Pattern Matching Using Automata (Alexey Bakhirkin, Thomas Ferrère, Dejan Nickovic, Oded Maler, Eugene Asarin)....Pages 215-232 Front Matter ....Pages 233-233 Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems (Susmit Jha, Sunny Raj, Sumit Kumar Jha, Natarajan Shankar)....Pages 235-251 Safe Over- and Under-Approximation of Reachable Sets for Autonomous Dynamical Systems (Meilun Li, Peter N. Mosaad, Martin Fränzle, Zhikun She, Bai Xue)....Pages 252-270 Tropical Abstractions of Max-Plus Linear Systems (Muhammad Syifa’ul Mufid, Dieky Adzkiya, Alessandro Abate)....Pages 271-287 Back Matter ....Pages 289-289 This book is based on the lectures given at the Oberwolfach Seminar on Tropical Algebraic Geometry in October 2004. Tropical Geometry?rst appeared as a subject of its own in 2002, while its roots can be traced back at least to Bergman's work [1] on logarithmic limit sets. Tropical Geometry is now a rapidly developing area of mathematics. It is int- twined with algebraic and symplectic geometry, geometric combinatorics, in- grablesystems, and statistical physics. Tropical Geometry can be viewed as a sort of algebraic geometry with the underlying algebra based on the so-called tropical numbers. The tropicalnumbers (the term “tropical” comesfrom computer science and commemorates Brazil, in particular a contribution of the Brazilian school to the language recognition problem) are the real numbers enhanced with negative in?nity and equipped with two arithmetic operations called tropical addition and tropical multiplication. The tropical addition is the operation of taking the m- imum. The tropical multiplication is the conventional addition. These operations are commutative, associative and satisfy the distribution law. It turns out that such tropical algebra describes some meaningful geometric objects, namely, the Tropical Varieties. From the topological point of view the tropical varieties are piecewise-linearpolyhedral complexes equipped with a particular geometric str- ture coming from tropical algebra. From the point of view of complex geometry this geometric structure is the worst possible degeneration of complex structure on a manifold. "This volume contains the proceedings of a workshop held in Grenoble in June 1989. This was the first workshop entirely devoted to the verification of finite state systems. The workshop brought together researchers and practitioners interested in the development and use of methods, tools and theories for automatic verification of finite state systems. The goal at the workshop was to compare verification methods and tools to assist the applications designer. The papers in this volume review verification techniques for finite state systems and evaluate their relative advantages. The techniques considered cover various specification formalisms such as process algebras, automata and logics. Most of the papers focus on exploitation of existing results in three application areas: hardware design, communication protocols and real-time systems."--Publisher's website Annotation This volume contains the proceedings of a workshop held in Grenoble in June 1989. This was the first workshop entirely devoted to the verification of finite state systems. The workshop brought together researchers and practitioners interested in the development and use of methods, tools and theories for automatic verification of finite state systems. The goal at the workshop was to compare verification methods and tools to assist the applications designer. The papers in this volume review verification techniques for finite state systems and evaluate their relative advantages. The techniques considered cover various specification formalisms such as process algebras, automata and logics. Most of the papers focus on exploitation of existing results in three application areas: hardware design, communication protocols and real-time systems Tropical geometry is algebraic geometry over the semifield of tropical numbers, i.e., the real numbers and negative infinity enhanced with the (max, +)-arithmetics. Geometrically, tropical varieties are much simpler than their classical counterparts. Yet they carry information about complex and real varieties. These notes present an introduction to tropical geometry and contain some applications of this rapidly developing and attractive subject. It consists of three chapters which complete each other and give a possibility for non-specialists to make the first steps in the subject which is not yet well represented in the literature. The intended audience is graduate, post-graduate, and Ph. D. students as well as established researchers in mathematics The book constitutes the refereed proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007, held in Nice, France in January 2007, co-located with the Symposium on Principles of Programming Languages (POPL 2007). The 21 revised full papers presented together with 3 invited lectures and 3 invited tutorials were carefully reviewed and selected from a total of 85 submissions. The papers feature current research from the communities of verification, model checking, and abstract interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods The book constitutes the refereed proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007, held in Nice, France in January 2007. This event was co-located with the Symposium on Principles of Programming Languages (POPL 2007). The 21 revised full papers presented together with three invited lectures and three invited tutorials were carefully reviewed and selected from a total of 85 submissions. The theory of process calculi as started with CCS [Mil 80] resulted in a number of verification tools designs, mostly in the case of terms with finitary representation (finite automata) [CPS 89,BoC 88,GLZ 89].