02106nam 2200349Ia 450 99638977140331620210104171956.0(CKB)4940000000095445(EEBO)2240872013(OCoLC)ocm80922569e(OCoLC)80922569(EXLCZ)99494000000009544520070131d1693 uy 0engurbn||||a|bb|Proposals for printing by subscription, the second, third and fourth volumes of the French Book of martyrs, or History of the famous Edict of Nantes[electronic resource] Which three volumes with the first already publish'd, contain an account of all the persecutions that have been in France, from the beginning of the Reformation (there) down to the present time, comprehending the reigns of Henry III. Henry IV. Lewis XIII. and Lewis XIV. The whole work faithfully extracted from all the publick and secret memoirs that cou'd possibly be procured, by that learned and judicious divine Mounsieur Bennoit. Printed first in French by the authority of the states of Holland and West-Friezland, and now translated into English. With Her Majesties royal priviledge[London] Printed for John Dunton at the Raven in the Poultrey.[1693]1 sheet ([2] p.)"Proposals are to be had of the undertaker John Dunton at the Raven in the Poultrey, and of most booksellers in London and the countrey"--P. [2].Place and date of publication suggested by Wing.Reproduction of original in the Boston Public Library.eebo-0015Publishers and publishingEnglandEarly works to 1800BroadsidesEngland17th century.rbgenrPublishers and publishingDunton John1659-1733.1001738UMIUMIBOOK996389771403316Proposals for printing by subscription, the second, third and fourth volumes of the French Book of martyrs, or History of the famous Edict of Nantes2299123UNISA09975nam 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 Systems772562UNISA