Linked e-resources
Details
Table of Contents
Intro; Preface; Organization; Abstracts of Invited Talks; Bidding Games on Markov Decision Processes; The Reachability Problem for Petri Nets is Not Elementary; Primitivity and Synchronizing Automata: A Functional Analytic Approach; Game Graphs for Reactive Synthesis; Reaching Out Towards Fully Verified Autonomous Systems; Contents; Bidding Games on Markov Decision Processes; 1 Introduction; 2 Preliminaries; 3 Qualitative Bidding Games on MDPs; 4 Mean-Payoff Bidding Games on Strongly-Connected MDPs; 5 Discussion; References
Primitivity and Synchronizing Automata: A Functional Analytic Approach1 Introduction; 2 Contraction Operators and Reachability Theorems; 3 Contractive Families and Functional Equations; 4 m-primitivity and m-syncronising Automata; References; Reaching Out Towards Fully Verified Autonomous Systems; 1 Introduction; 2 Preliminaries: Neural Networks; 2.1 Neural Networks; 3 Verification of Neural Networks; 3.1 Abstract Interpretation for Neural Networks; 3.2 Training with Robustness; 3.3 Closed Loop Verification; 3.4 Falsification and Testing; 4 Challenges; 5 Conclusion; References
On the m-eternal Domination Number of Cactus Graphs1 Introduction; 2 The m-eternal Domination of Christmas Cactus Graphs; 3 Upper Bound on the m-eternal Domination Number of Cactus Graphs; 4 Linear-Time Algorithm; 5 Future Work; References; On Relevant Equilibria in Reachability Games; 1 Introduction; 2 Preliminaries and Studied Problems; 3 Existence Problems; 4 Solving Decision Problems; 4.1 -Consistent Play; 4.2 Characterizations; 4.3 Sufficiency of Lassoes; 4.4 Algorithms; 4.5 Results; References; Partial Solvers for Generalized Parity Games; 1 Introduction; 2 Preliminaries
3 Zielonka's Algorithm with Partial Solvers4 Algorithms BüchiSolver and GenBüchiSolver; 5 Algorithms GoodEpSolver and GenGoodEpSolver; 6 Algorithms LaySolver and GenLaySolver; 7 Empirical Evaluation; References; Reachability in Augmented Interval Markov Chains; 1 Introduction; 2 Preliminaries; 3 Qualitative Case; 4 Quantitative Case: Upper Bound; 5 Quantitative Case: Lower Bound; 6 Approximate Case; References; On Solving Word Equations Using SAT; 1 Introduction; 2 Preliminaries; 3 Word Equation Solving; 3.1 Solving Bounded Word Equation; 3.2 Refining Bounds and Guiding the Search
4 Experiments5 Conclusion; References; Parameterised Verification of Publish/Subscribe Networks with Exception Handling; 1 Introduction; 2 Formal Model of Pub/Sub Architectures; 2.1 Pub/Sub Networks; 3 Example: Specification of an IoT System; 4 The Coverability Decision Problem; 4.1 Decision Procedure for Coverability in Pub/Sub Networks; 5 Notification with Retained Messages; 6 Handling Exceptions During Notifications; 7 Conclusions; References; Cellular Automata for the Self-stabilisation of Colourings and Tilings; 1 Introduction; 2 Setting of the Problem; 3 The Case of 2-Colourings
Primitivity and Synchronizing Automata: A Functional Analytic Approach1 Introduction; 2 Contraction Operators and Reachability Theorems; 3 Contractive Families and Functional Equations; 4 m-primitivity and m-syncronising Automata; References; Reaching Out Towards Fully Verified Autonomous Systems; 1 Introduction; 2 Preliminaries: Neural Networks; 2.1 Neural Networks; 3 Verification of Neural Networks; 3.1 Abstract Interpretation for Neural Networks; 3.2 Training with Robustness; 3.3 Closed Loop Verification; 3.4 Falsification and Testing; 4 Challenges; 5 Conclusion; References
On the m-eternal Domination Number of Cactus Graphs1 Introduction; 2 The m-eternal Domination of Christmas Cactus Graphs; 3 Upper Bound on the m-eternal Domination Number of Cactus Graphs; 4 Linear-Time Algorithm; 5 Future Work; References; On Relevant Equilibria in Reachability Games; 1 Introduction; 2 Preliminaries and Studied Problems; 3 Existence Problems; 4 Solving Decision Problems; 4.1 -Consistent Play; 4.2 Characterizations; 4.3 Sufficiency of Lassoes; 4.4 Algorithms; 4.5 Results; References; Partial Solvers for Generalized Parity Games; 1 Introduction; 2 Preliminaries
3 Zielonka's Algorithm with Partial Solvers4 Algorithms BüchiSolver and GenBüchiSolver; 5 Algorithms GoodEpSolver and GenGoodEpSolver; 6 Algorithms LaySolver and GenLaySolver; 7 Empirical Evaluation; References; Reachability in Augmented Interval Markov Chains; 1 Introduction; 2 Preliminaries; 3 Qualitative Case; 4 Quantitative Case: Upper Bound; 5 Quantitative Case: Lower Bound; 6 Approximate Case; References; On Solving Word Equations Using SAT; 1 Introduction; 2 Preliminaries; 3 Word Equation Solving; 3.1 Solving Bounded Word Equation; 3.2 Refining Bounds and Guiding the Search
4 Experiments5 Conclusion; References; Parameterised Verification of Publish/Subscribe Networks with Exception Handling; 1 Introduction; 2 Formal Model of Pub/Sub Architectures; 2.1 Pub/Sub Networks; 3 Example: Specification of an IoT System; 4 The Coverability Decision Problem; 4.1 Decision Procedure for Coverability in Pub/Sub Networks; 5 Notification with Retained Messages; 6 Handling Exceptions During Notifications; 7 Conclusions; References; Cellular Automata for the Self-stabilisation of Colourings and Tilings; 1 Introduction; 2 Setting of the Problem; 3 The Case of 2-Colourings