09975nam 2200529 450 99648566540331620230113164508.03-031-15839-3(MiAaPQ)EBC7078240(Au-PeEL)EBL7078240(CKB)24750399800041(PPN)264191587(EXLCZ)992475039980004120230113d2022 uy 0engurcnu||||||||txtrdacontentcrdamediacrrdacarrierFormal modeling and analysis of timed systems 20th international conference, FORMATS 2022, Warsaw, Poland, September 13-15, 2022, proceedings /Sergiy Bogomolov, David Parker (editors)Cham, Switzerland :Springer,[2022]©20221 online resource (315 pages)Lecture notes in computer science ;Volume 13465Print version: Bogomolov, Sergiy Formal Modeling and Analysis of Timed Systems Cham : Springer International Publishing AG,c2022 9783031158384 Intro -- Preface -- Organization -- Abstracts -- A Behaviour-Based Approach to Quantitative Validation of Cyber-Physical Systems -- A Personal History of Formal Modeling and Analysis of Timed Systems Before There was FORMATS -- Contents -- Invited Papers -- Algebraic Model Checking for Discrete Linear Dynamical Systems -- 1 Introduction -- 1.1 Skolem Oracles -- 1.2 Main Results -- 2 Algebraic Model Checking -- 3 Conclusion -- References -- Zone-Based Verification of Timed Automata: Extrapolations, Simulations and What Next? -- 1 Introduction -- 2 Birth of Timed Automata for Verification: The Early 90's -- 2.1 Preliminaries -- 2.2 The Timed Automaton Model ch2AD90,ch2AD94 -- 3 A Symbolic Approach to the Verification of Timed Automata -- 3.1 Zones and Symbolic Forward Computation -- 3.2 Difference Bounded Matrices (DBMs) -- 3.3 Efficiency of the Forward Analysis -- 4 Extrapolation: A First Solution -- 4.1 The First Extrapolation Operator -- 4.2 Two Refinements of This Approach -- 4.3 Problems with Diagonal Clock Constraints -- 5 Simulation: An Alternative Solution -- 6 Beyond Reachability -- 6.1 Weighted Timed Automata -- 6.2 Liveness Properties -- 7 Tools -- 7.1 A Tool for Verifying Timed Automata: Uppaal -- 7.2 The Tool TChecker -- 8 What Next? -- 8.1 BDD and SAT Based Methods -- 8.2 The Local-Time Semantics and Partial-Order Reduction -- 8.3 Domain-Specific Algorithms -- 8.4 Richer Models -- References -- Monitoring Timed Properties (Revisited) -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 4 Monitoring in a Timed Setting -- 5 Time Divergence -- 6 A Symbolic Method for Monitoring -- 7 Time Uncertainty -- 8 Time Predictive Monitoring -- 9 Conclusion -- References -- Probabilistic and Timed Systems -- Bounded Delay Timed Channel Coding -- 1 Introduction -- 2 Preliminary Work -- 2.1 Timed Languages and Timed Automata.2.2 Entropy and Capacity -- 2.3 Pseudo-Distance on Timed Languages -- 2.4 The Factor Language -- 3 Bandwidth -- 3.1 Definitions -- 3.2 Examples -- 3.3 Existence of Limits -- 4 Encodings -- 4.1 Definition -- 4.2 Necessary Condition -- 4.3 Sufficient Condition -- 5 Conclusion and Further Work -- References -- Robustly Complete Finite-State Abstractions for Verification of Stochastic Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Canonical Sample Space -- 2.2 Markov Transition Systems -- 2.3 Weak Convergence and Prokhorov's Theorem -- 2.4 Discrete-Time Continuous-State Stochastic Systems -- 2.5 Robust Abstractions -- 3 Soundness of Robust IMC Abstractions -- 3.1 Weak Compactness of Marginal Space Mt of Probabilities -- 3.2 Weak Compactness of Probability Laws of I on Infinite Horizon -- 3.3 Soundness of IMC Abstractions -- 4 Robust Completeness of IMC Abstractions -- 5 Conclusion -- References -- Model Checking for Entanglement Swapping -- 1 Introduction -- 2 Preliminaries -- 2.1 Probabilistic Timed Automata -- 3 Modeling and Validation -- 3.1 The PTA Model -- 3.2 Validation Through Simulations -- 4 Experimental Setup -- 5 Results -- 6 Discussions and Outlook -- References -- Temporal Logic -- An STL-Based Formulation of Resilience in Cyber-Physical Systems -- 1 Introduction -- 2 Preliminaries -- 3 Specifying Resilience in STL -- 3.1 Resiliency Specification Language -- 3.2 Semantics of Resiliency Specifications -- 4 Case Study -- 4.1 UAV Package Delivery -- 4.2 Multi-agent Flocking -- 5 Related Work -- 6 Conclusion -- References -- MITL Verification Under Timing Uncertainty -- 1 Introduction -- 2 Preliminaries -- 2.1 Set Theory -- 2.2 Topology -- 3 Problem Formulation -- 3.1 Syntax and Semantics of MITL -- 3.2 Truth Sets and Interval Queues -- 4 Interval Queue Fundamentals -- 4.1 Construction Algorithm -- 4.2 Complementation Algorithm.5 Verification Procedure -- 5.1 Operators in the Interval Queue Domain -- 5.2 Constructing Under- and Over-Approximations -- 5.3 Conservativeness -- 6 Numerical Example -- 7 Conclusion -- A Proof of Theorem 1 -- References -- Classification of Driving Behaviors Using STL Formulas: A Comparative Study -- 1 Introduction -- 2 Preliminaries -- 3 Specifying Longitudinal Driving Behavior with STL -- 4 Methods -- 5 Experiments -- 6 Discussion and Conclusions -- References -- Timed Automata and Games -- Timed Games with Bounded Window Parity Objectives -- 1 Introduction -- 2 Preliminaries -- 3 Bounded Window Objectives -- 4 Verification of Timed Automata -- 5 Solving Timed Games -- References -- Non-blind Strategies in Timed Network Congestion Games -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Network Congestion Game -- 2.2 Studied Problems -- 3 Existence and Computation of Nash Equilibria -- 3.1 Transformation into an Equivalent Finite Concurrent Game -- 3.2 Existence of Nash Equilibria -- 3.3 Computation of Nash Equilibria -- 4 Social Optimality and Prices of Anarchy and Stability -- 4.1 Constrained-Social-Welfare Problem: Asymmetric Case -- 4.2 Constrained-Social-Welfare Problem: Symmetric Case -- 4.3 Social Optimum and Prices of Anarchy and Stability -- References -- Efficient Convex Zone Merging in Parametric Timed Automata -- 1 Introduction -- 2 Preliminaries -- 3 Efficient State Merging in Parametric Timed Automata -- 3.1 Merging Algorithm -- 3.2 Heuristics for Merging -- 3.3 Preservation of Properties -- 4 Experiments -- 4.1 Dataset and Experimental Environment -- 4.2 Description of the Experiments -- 5 Conclusion -- A Results for All Heuristics on the Full Benchmark -- References -- Neural Networks -- Neural Network Repair with Reachability Analysis -- 1 Introduction -- 2 Deep Neural Network Repair -- 2.1 Provably Safe DNNs.2.2 DNN Agent Repair for Deep Reinforcement Learning -- 2.3 Computation of Exact Unsafe Domain of ReLU DNNs -- 3 Framework for DNN Repair -- 3.1 Formulation of Loss Function for Problems 1 &amp -- 2 -- 3.2 Repair for Deep Reinforcement Learning -- 4 Experiments and Evaluation -- 4.1 Repair of ACAS Xu Neural Network Controllers -- 4.2 Rocket Lander Benchmark -- 5 Conclusion and Future Work -- References -- On Neural Network Equivalence Checking Using SMT Solvers -- 1 Introduction -- 2 Preliminaries: Neural Networks -- 2.1 Notation -- 2.2 Neural Networks -- 3 Strict and Approximate Equivalences for Neural Networks -- 3.1 Strict Neural Network Equivalence -- 3.2 Approximate Neural Network Equivalences Based on Lp Norms -- 3.3 Approximate Neural Network Equivalences Based on Order of Outputs -- 3.4 Hybrid Lp-argsort Equivalences -- 3.5 The Neural Network Equivalence Checking Problem -- 3.6 Discussion of Application Domains for the Above Equivalence Relations -- 4 Neural Network Equivalence Checking Using SMT Solvers -- 4.1 Encoding Neural Networks as SMT Formulas -- 4.2 Encoding of the Equivalence Relation -- 4.3 Optimizing the Encoding -- 5 Experimental Results -- 5.1 Sanity Checks -- 5.2 Equivalence Checking -- 6 Related Work -- 7 Conclusions -- References -- Reachability Analysis of a General Class of Neural Ordinary Differential Equations -- 1 Introduction -- 2 Background and Problem Formulation -- 2.1 General Neural ODE -- 2.2 NODE: Applications -- 2.3 Reachability Analysis -- 2.4 Reachability Methods -- 3 Evaluation -- 3.1 Method and Tool Comparison -- 3.2 Case Study: Adaptive Cruise Control (ACC) -- 3.3 Classification NODEs -- 4 Related Work -- 5 Conclusion and Future Work -- References -- Reinforcement Learning -- Robust Event-Driven Interactions in Cooperative Multi-agent Learning -- 1 Introduction -- 1.1 Main Contribution -- 2 Preliminaries.2.1 Notation -- 2.2 MDPs and Multi-agent MDPs -- 2.3 Value Functions and Q-Learning in c-MMDPs -- 3 Information Sharing Between Collaborative Agents: Problem Formulation -- 4 Efficient Communication Strategies -- 4.1 Event-Driven Interactions -- 5 Robustness Surrogate and Its Computation -- 5.1 Learning the Robustness Surrogate with the Scenario Approach -- 6 Experiments -- 6.1 Benchmark: Collaborative Particle-Tag -- 6.2 Computation of Robustness Surrogates -- 6.3 Results -- 7 Discussion -- References -- Learning that Grid-Convenience Does Not Hurt Resilience in the Presence of Uncertainty -- 1 Introduction -- 2 Case Study -- 3 Methodology -- 4 Results -- 5 Reproducibility and Conclusions -- References -- Author Index.Lecture notes in computer science ;Volume 13465.Computer simulationCongressesFormal methods (Computer science) CongressesSystem analysisCongressesComputer simulationFormal methods (Computer science) System analysis003.3Bogomolov SergiyParker DavidMiAaPQMiAaPQMiAaPQBOOK996485665403316Formal Modeling and Analysis of Timed Systems772562UNISA03933nam 2200685Ia 450 991096543650332120200520144314.09786613134950978030921585503092158549781283134958128313495097803091596300309159636(CKB)2550000000037259(EBL)3378780(SSID)ssj0000524684(PQKBManifestationID)12179460(PQKBTitleCode)TC0000524684(PQKBWorkID)10500183(PQKB)10715518(MiAaPQ)EBC3378780(Au-PeEL)EBL3378780(CaPaEBR)ebr10478230(CaONFJC)MIL313495(OCoLC)923282431(Perlego)4734381(EXLCZ)99255000000003725920101115d2010 uy 0engurcn|||||||||txtccrNew worlds, new horizons in astronomy and astrophysics /Science Frontiers Panels, Committee for a Decadal Survey of Astronomy and Astrophysics, Board on Physics and Astronomy, Space Studies Board, Division on Engineering and Physical Sciences1st ed.Washington, D.C. National Academies Press20101 online resource (577 p.)Panel reportsDescription based upon print version of record.9780309159623 0309159628 ""Front Matter""; ""Preface""; ""Acknowledgment of Members of the Astro 2010 Infrastructure Study Groups""; ""Acknowledgment of Reviewers""; ""Contents""; ""Part I: Reports of the Astro 2010 Science Frontiers Panels""; ""1 Report of the Panel on Cosmology and Fundamental Physics""; ""2 Report of the Panel on the Galactic Neighborhood""; ""3 Report of the Panel on Galaxies Across Cosmic Time""; ""4 Report of the Panel on Planetary Systems and Star Formation""; ""5 Report of the Panel on Stars and Stellar Evolution""; ""Summary Findings""""Part II: Reports of the Astro 2010 Program Prioritization Panels""""6 Report of the Panel on Electromagnetic Observations from Space""; ""7 Report of the Panel on Optical and Infrared Astronomy from the Ground""; ""8 Report of the Panel on Particle Astrophysics and Gravitation""; ""9 Report of the Panel on Radio, Millimeter, and Submillimeter Astronomy from the Ground""; ""Appendixes""; ""Appendix A: Statements of Task for the Astro2010 Panels""; ""Appendix B: Glossary""; ""Appendix C Acronyms"""Panel Reports--New Worlds, New Horizons in Astronomy and Astrophysics is a collection of reports, each of which addresses a key sub-area of the field, prepared by specialists in that subarea, and each of which played an important role in setting overall priorities for the field ... The Committee for a Decadal Survey of Astronomy and Astrophysics synthesized these reports in the preparation of its prioritized recommendations for the field as a whole. These reports provide additional depth and detail in each of their respective areas. Taken together, they form an essential companion volume to New Worlds, New Horizons: A Decadal Survey of Astronomy and Astrophysics."--National Academies Press website.AstronomyResearchForecastingAstrophysicsResearchForecastingResearchInternational cooperationAstronomyResearchForecasting.AstrophysicsResearchForecasting.ResearchInternational cooperation.520National Research Council (U.S.).Science Frontiers Panels.MiAaPQMiAaPQMiAaPQBOOK9910965436503321New worlds, new horizons in astronomy and astrophysics4367622UNINA