Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday (Lecture Notes in Computer Science Book 10460)

This Festschrift is published in honor of Kim Guldstrand Larsen, one of the earliest precursors of computer science in Denmark, on the occasion of his 60th birthday. During the last three decades, Kim Guldstrand Larsen has given major contributions across a remarkably wide range of topics, including real-time, concurrent, and probabilistic models of computation, logic in computer science, and model checking. Since 1995, he has been one of the prime movers behind the model checking tool for real-time systems UPPAAL, for which he was a co-recipient of the CAV Award in 2013. The Festschrift contains 32 papers that feature the broad range of Kim Guldstrand Larsen's research topics, such as formal languages and automata theory; logic; verification, model checking and testing; algorithmic game theory and mechanism design; semantics and reasoning; real-time and distributed systems; and modeling and simulation. Front Matter ....Pages I-XVII Front Matter ....Pages 1-1 Information Flow for Timed Automata (Flemming Nielson, Hanne Riis Nielson, Panagiotis Vasilikos)....Pages 3-21 A Nivat Theorem for Quantitative Automata on Unranked Trees (Manfred Droste, Doreen Götze)....Pages 22-35 30 Years of Modal Transition Systems: Survey of Extensions and Analysis (Jan Křetínský)....Pages 36-74 Derivatives of Quantitative Regular Expressions (Rajeev Alur, Konstantinos Mamouras, Dogan Ulus)....Pages 75-95 Improving the Timed Automata Approach to Biological Pathway Dynamics (Rom Langerak, Jaco van de Pol, Janine N. Post, Stefano Schivo)....Pages 96-111 Bicategories of Markov Processes (Florence Clerc, Harrison Humphrey, Prakash Panangaden)....Pages 112-124 Property-Preserving Parallel Decomposition (Bernhard Steffen, Marc Jasper)....Pages 125-145 A Generic Algorithm for Learning Symbolic Automata from Membership Queries (Oded Maler, Irini-Eleftheria Mens)....Pages 146-169 Teaching Academic Concurrency to Amazing Students (Sebastian Biewer, Felix Freiberger, Pascal Leo Held, Holger Hermanns)....Pages 170-195 Front Matter ....Pages 197-197 Negative Results on Decidability and Small Model Property of Process Equations (Xinxin Liu)....Pages 199-210 Timed Temporal Logics (Patricia Bouyer, François Laroussinie, Nicolas Markey, Joël Ouaknine, James Worrell)....Pages 211-230 Front Matter ....Pages 231-231 Synchronous Interfaces and Assume/Guarantee Contracts (Albert Benveniste, Benoît Caillaud)....Pages 233-248 From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL (Aleksandar S. Dimovski, Andrzej Wąsowski)....Pages 249-268 Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking (Anders P. Ravn, Bent Thomsen, Kasper Søe Luckow, Lone Leth, Thomas Bøgholm)....Pages 269-288 Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata (Marta Kwiatkowska, Gethin Norman, David Parker)....Pages 289-309 Runtime Verification Logics A Language Design Perspective (Klaus Havelund, Giles Reger)....Pages 310-338 Testing Divergent Transition Systems (Ed Brinksma, Mariëlle I. A. Stoelinga, Mark Timmer)....Pages 339-366 The Cost of Exactness in Quantitative Reachability (Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger)....Pages 367-381 Towards Automated Variant Selection for Heterogeneous Tiled Architectures (Christel Baier, Sascha Klüppelholz, Sascha Wunderlich)....Pages 382-399 Front Matter ....Pages 401-401 Admissible Strategies in Timed Games (Nicolas Basset, Jean-François Raskin, Ocan Sankur)....Pages 403-425 Modal Stochastic Games (Joost-Pieter Katoen, Falak Sher)....Pages 426-445 Front Matter ....Pages 447-447 A Coinductive Equational Characterisation of Trace Inclusion for Regular Processes (Matthew Hennessy)....Pages 449-465 Syntactic Markovian Bisimulation for Chemical Reaction Networks (Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin)....Pages 466-483 Assertion-Based Reasoning Method for Calculus of Wireless System (Luyao Wang, Wanling Xie, Huibiao Zhu)....Pages 484-502 Taming Living Logic Using Formal Methods (Hasan Baig, Jan Madsen)....Pages 503-515 Comparing Source Sets and Persistent Sets for Partial Order Reduction (Parosh Abdulla, Stavros Aronis, Bengt Jonsson, Konstantinos Sagonas)....Pages 516-536 Front Matter ....Pages 537-537 A Framework for Evaluating Schedulability Analysis Tools (Lijun Shan, Susanne Graf, Sophie Quinton, Loïc Fejoz)....Pages 539-559 WUPPAAL: Computation of Worst-Case Execution-Time for Binary Programs with UPPAAL (Franck Cassez, Pablo Gonzalez de Aledo, Peter Gjøl Jensen)....Pages 560-577 Centrally Governed Blockchains: Optimizing Security, Cost, and Availability (Leif-Nissen Lundbæk, Andrea Callia D’Iddio, Michael Huth)....Pages 578-599 Front Matter ....Pages 601-601 Energy Consumption Forecast of Photo-Voltaic Comfort Cooling Using UPPAAL Stratego (Mads Kronborg Agesen, Søren Enevoldsen, Thibaut Le Guilly, Anders Mariegaard, Petur Olsen, Arne Skou)....Pages 603-622 Towards a Tool: TIMES-Pro for Modeling, Analysis, Simulation and Implementation of Cyber-Physical Systems (Jakaria Abdullah, Gaoyang Dai, Nan Guan, Morteza Mohaqeqi, Wang Yi)....Pages 623-639 Formalising a Hazard Warning Communication Protocol with Timed Automata (Ernst-Rüdiger Olderog, Maike Schwammberger)....Pages 640-660 Back Matter ....Pages 661-662