Computer Aided Verification : : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.14683 |
---|---|
: | |
TeilnehmendeR: | |
Place / Publishing House: | Cham : : Springer International Publishing AG,, 2024. ©2024. |
Year of Publication: | 2024 |
Edition: | 1st ed. |
Language: | English |
Series: | Lecture Notes in Computer Science Series
|
Physical Description: | 1 online resource (597 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
993687476404498 |
---|---|
ctrlnum |
(CKB)33600912200041 (MiAaPQ)EBC31594174 (Au-PeEL)EBL31594174 (EXLCZ)9933600912200041 |
collection |
bib_alma |
record_format |
marc |
spelling |
Gurfinkel, Arie. Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. 1st ed. Cham : Springer International Publishing AG, 2024. ©2024. 1 online resource (597 pages) text txt rdacontent computer c rdamedia online resource cr rdacarrier Lecture Notes in Computer Science Series ; v.14683 Description based on publisher supplied metadata and other sources. Intro -- Preface -- Organization -- Invited Talks -- How to Solve Math Problems Without Talent -- Bridging Formal Mathematics and Software Verification -- The Art of SMT Solving -- Contents - Part III -- Synthesis and Repair -- Syntax-Guided Automated Program Repair for Hyperproperties -- 1 Introduction -- 2 Preliminaries -- 3 Program Repair by Symbolic Execution -- 3.1 Symbolic Execution -- 3.2 Symbolic Paths and Safety Automata -- 3.3 Encoding for HyperLTL -- 3.4 Program Repair Using SyGuS -- 4 Transparent Repair -- 4.1 Transparency -- 4.2 Encoding for Transparent Repair -- 5 Iterative Repair -- 5.1 Encoding for Iterative Repair -- 5.2 Iterative Repair Loop -- 6 Implementation and Evaluation -- 6.1 Iterative Repair for Hyperproperties -- 6.2 Scalability in Solution Size -- 6.3 Evaluation on k-Safety Instances -- 6.4 Evaluation on Functional Properties -- 7 Related Work -- 8 Conclusion -- References -- The SemGuS Toolkit -- 1 Introduction -- 2 The SemGuS Format 1.0 -- 3 A Baseline SemGuS Solver -- 3.1 Verifying Candidate Solutions -- 3.2 Baseline Enumerative Solvers -- 3.3 Extensibility -- 4 Benchmarks and Performance of Baseline Solvers -- 5 Related Work -- References -- Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries -- 4 Constraint Annotated Tree Automata -- 4.1 CATA Operations for Synthesis -- 5 Synthesis Algorithm -- 5.1 Problem Statement -- 5.2 Basic Synthesis Algorithm -- 5.3 Lazy Synthesis Algorithm -- 6 Implementation -- 7 Evaluation -- 8 Related Work -- 9 Conclusion -- References -- Information Flow Guided Synthesis with Unbounded Communication -- 1 Introduction -- 2 Running Example: Sequence Transmission -- 3 Preliminaries -- 4 Prefix Information Flow -- 5 Unbounded Communication in Distributed Systems -- 5.1 Receiving Information. 5.2 Transmitting Information -- 5.3 Safety Hyper Implementations -- 6 Synthesis with Prefix Information Flow Assumptions -- 6.1 Automata for Assume and Guarantee Specifications -- 6.2 Compositional Synthesis -- 7 Experiments -- 8 Related Work -- 9 Conclusion -- References -- Synthesis of Temporal Causality -- 1 Introduction -- 1.1 Temporal Causality -- 1.2 Contributions and Structure -- 2 Preliminaries -- 3 Overview: The Topology of Causality -- 3.1 Actual Causes as Downward Closed Sets of Traces -- 3.2 Causality Without the Limit Assumption -- 4 Generalized Temporal Causality -- 4.1 Similarity Relations and the Limit Assumption -- 4.2 A General Definition of Temporal Causality -- 4.3 Proving Generalization -- 5 Cause Synthesis -- 5.1 Proving Our Characterization -- 5.2 Cause-Synthesis Algorithm for -Regular Effects -- 6 Implementation and Evaluation -- 6.1 Cause Synthesis -- 6.2 Cause Checking -- 7 Related Work -- 8 Conclusion -- References -- Dynamic Programming for Symbolic Boolean Realizability and Synthesis -- 1 Introduction -- 2 Preliminary Definitions -- 2.1 Boolean Formula and Synthesis Concepts -- 2.2 Dynamic Programming Concepts - Project-Join Trees -- 3 Realizability CheckingProofs for All Lemmas and Theorems Can Be Found in the Appendix A. -- 3.1 Theoretical Basis and Valuations in Trees -- 3.2 Determining Nullary, Partial and Full Realizability -- 4 Synthesis of Witness Functions -- 4.1 Monolithic Approach -- 4.2 Synthesis Using Graded Project-Join Trees -- 5 Experimental Evaluation -- 5.1 Realizability-Checking Phase -- 5.2 Synthesis -- 5.3 Tree Widths and Realizability -- 5.4 Comparison with Non-BDD-Based Synthesis -- 6 Concluding Remarks -- References -- Localized Attractor Computations for Infinite-State Games -- 1 Introduction -- 2 Preliminaries -- 3 Attractor Computation with Caching -- 4 Abstract Template-Based Cache Generation. 4.1 Generating Attractor Caches from Sub-Games -- 4.2 Constructing Sub-games from Abstract Strategy Templates -- 5 Game Solving with Abstract Template-Based Caching -- 6 Experimental Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Learning -- Bisimulation Learning -- 1 Introduction -- 2 Illustrative Example -- 3 Stutter-Insensitive Bisimulations of Deterministic Transition Systems -- 3.1 Model Checking -- 4 Counterexample-Guided Bisimulation Learning -- 4.1 Learner-Verifier Framework for Bisimulation Learning -- 4.2 Binary Decision Tree Partition Templates -- 5 Experimental Evaluation -- 5.1 Discrete-Time Clock Synchronization -- 5.2 Conditional Termination -- 6 Conclusion -- References -- Regular Reinforcement Learning -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Regular Languages -- 3.2 Rational Transductions -- 3.3 Markov Decision Processes -- 4 Regular Markov Decision Processes -- 4.1 Undecidability of Values -- 4.2 Discounted Optimization -- 4.3 Finiteness Conditions -- 4.4 Q-Learning in RMDPs -- 5 Deep Regular Reinforcement Learning -- 5.1 Token Passing -- 5.2 Duplicating Pebbles -- 5.3 Shunting Yard Algorithm -- 5.4 Modified Tangrams -- 6 Conclusion -- References -- LTL Learning on GPUs -- 1 Introduction -- 2 Formal Preliminaries -- 3 High-Level Structure of the Algorithm -- 4 In-Memory Representation of Search Space -- 5 Correctness and Complexity of the Branch-Free Implementation of Temporal Operators -- 6 Relaxed Uniqueness Checks -- 7 Divide & -- Conquer -- 8 Evaluation of Algorithm Performance -- 9 Conclusion -- References -- Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models -- 1 Introduction -- 2 Problem Setup -- 3 Verified Exploration Through Learned Models -- 3.1 Symbolic Environment Models -- 3.2 Shielding for Verified Safe Exploration. 3.3 Neural Controller Approximation -- 4 Experiments -- 5 Related Work -- 6 Conclusion -- References -- Cyberphysical and Hybrid Systems -- Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems -- 1 Introduction -- 1.1 Related Work -- 1.2 Contributions -- 2 Preliminaries and Problem Statement -- 2.1 Intervals -- 2.2 Truth Values -- 2.3 Signals -- 2.4 Reachability Analysis of Hybrid Systems -- 2.5 Signal Temporal Logic with Boolean Semantics -- 2.6 Problem Statement -- 3 Basic Idea and Solution Concept -- 4 Four-Valued Signal Temporal Logic -- 4.1 Computing Boolean Satisfaction Signals -- 4.2 Computing Three-Valued Satisfaction Signals -- 4.3 Computing Four-Valued Satisfaction Signals -- 5 Incremental Verification of Hybrid Systems -- 5.1 Incremental Verification Algorithm -- 5.2 Refinement via Branching the Reachability Analysis -- 6 Evaluation -- 6.1 Bouncing Ball -- 6.2 Autonomous Driving -- 6.3 Genetic Oscillator -- 7 Conclusion -- References -- Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications -- 1 Introduction -- 2 Preliminaries -- 2.1 Signal Temporal Logic -- 2.2 Finite Variability -- 3 Problem Formulation -- 4 Variable-Interval Encoding of STL to MILP -- 4.1 -Stable Partitions -- 4.2 Variable-Interval MILP Encoding -- 5 System Models and Their MILP Encoding -- 5.1 HAs with Closed-Form Solutions -- 5.2 HAs with Double Integrator Dynamics -- 6 Implementation and Experiments -- References -- Inner-Approximate Reachability Computation via Zonotopic Boundary Analysis -- 1 Introduction -- 2 Preliminaries -- 2.1 Notation -- 2.2 Problem Statement -- 3 Methodology -- 3.1 Inner-Approximation Computation Framework -- 3.2 Extraction of Zonotopes' Boundaries -- 3.3 Zonotopal Tiling and Boundary Refinement -- 3.4 Contracting Computed Outer-Approximation -- 4 Experiments. 4.1 Advantage in Efficiency and Precision -- 4.2 Advantage in Long Time Horizons -- 4.3 Advantage in Big Initial Sets -- 5 Conclusion -- References -- Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs -- 1 Introduction -- 2 Background -- 2.1 Preliminaries -- 2.2 Motivating Example: A Multi-UAV System -- 3 Scenario-Based Formalism for Reconfigurable Systems -- 3.1 Scenario-Based System Modeling -- 3.2 Specifying System Requirements in Topology-Aware STL -- 4 Path-Oriented Optimization-Based System Falsification -- 4.1 Falsification Framework -- 4.2 Path Generation for Hierarchical Scenario Tasks -- 4.3 Optimization-Based Falsification for Paths -- 5 Implementation and Evaluation -- 5.1 Implementation and Research Questions -- 5.2 Experimental Evaluation and Analysis -- 5.3 Threats to Validity -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Probabilistic Systems -- Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games -- 1 Introduction -- 2 Preliminaries -- 3 Complete-Exploration Algorithm for Solving SGs -- 4 Partial-Exploration Algorithm for Solving SGs -- 5 Tool Description -- 6 Experimental Evaluation -- 6.1 Experimental Setup -- 6.2 Results -- 7 Conclusion -- References -- What Should Be Observed for Optimal Reward in POMDPs? -- 1 Introduction -- 2 Preliminaries -- 2.1 Markov Decision Processes (MDPs) -- 2.2 Partially Observable Markov Decision Processes -- 3 The Optimal Observability Problem -- 3.1 Problem Statement -- 3.2 Undecidability -- 4 Optimal Observability for Positional Strategies -- 4.1 Positional and Deterministic Strategies -- 4.2 Positional Randomized Strategies -- 5 Implementation and Experimental Evaluation -- 5.1 Solving Optimal Observability Problems with Parameter Synthesis Tools -- 5.2 Implementation and Setup -- 5.3 Experimental Results. 6 Conclusion and Future Work. Ganesh, Vijay. 3-031-65632-6 Lecture Notes in Computer Science Series |
language |
English |
format |
eBook |
author |
Gurfinkel, Arie. |
spellingShingle |
Gurfinkel, Arie. Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. Lecture Notes in Computer Science Series ; Intro -- Preface -- Organization -- Invited Talks -- How to Solve Math Problems Without Talent -- Bridging Formal Mathematics and Software Verification -- The Art of SMT Solving -- Contents - Part III -- Synthesis and Repair -- Syntax-Guided Automated Program Repair for Hyperproperties -- 1 Introduction -- 2 Preliminaries -- 3 Program Repair by Symbolic Execution -- 3.1 Symbolic Execution -- 3.2 Symbolic Paths and Safety Automata -- 3.3 Encoding for HyperLTL -- 3.4 Program Repair Using SyGuS -- 4 Transparent Repair -- 4.1 Transparency -- 4.2 Encoding for Transparent Repair -- 5 Iterative Repair -- 5.1 Encoding for Iterative Repair -- 5.2 Iterative Repair Loop -- 6 Implementation and Evaluation -- 6.1 Iterative Repair for Hyperproperties -- 6.2 Scalability in Solution Size -- 6.3 Evaluation on k-Safety Instances -- 6.4 Evaluation on Functional Properties -- 7 Related Work -- 8 Conclusion -- References -- The SemGuS Toolkit -- 1 Introduction -- 2 The SemGuS Format 1.0 -- 3 A Baseline SemGuS Solver -- 3.1 Verifying Candidate Solutions -- 3.2 Baseline Enumerative Solvers -- 3.3 Extensibility -- 4 Benchmarks and Performance of Baseline Solvers -- 5 Related Work -- References -- Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries -- 4 Constraint Annotated Tree Automata -- 4.1 CATA Operations for Synthesis -- 5 Synthesis Algorithm -- 5.1 Problem Statement -- 5.2 Basic Synthesis Algorithm -- 5.3 Lazy Synthesis Algorithm -- 6 Implementation -- 7 Evaluation -- 8 Related Work -- 9 Conclusion -- References -- Information Flow Guided Synthesis with Unbounded Communication -- 1 Introduction -- 2 Running Example: Sequence Transmission -- 3 Preliminaries -- 4 Prefix Information Flow -- 5 Unbounded Communication in Distributed Systems -- 5.1 Receiving Information. 5.2 Transmitting Information -- 5.3 Safety Hyper Implementations -- 6 Synthesis with Prefix Information Flow Assumptions -- 6.1 Automata for Assume and Guarantee Specifications -- 6.2 Compositional Synthesis -- 7 Experiments -- 8 Related Work -- 9 Conclusion -- References -- Synthesis of Temporal Causality -- 1 Introduction -- 1.1 Temporal Causality -- 1.2 Contributions and Structure -- 2 Preliminaries -- 3 Overview: The Topology of Causality -- 3.1 Actual Causes as Downward Closed Sets of Traces -- 3.2 Causality Without the Limit Assumption -- 4 Generalized Temporal Causality -- 4.1 Similarity Relations and the Limit Assumption -- 4.2 A General Definition of Temporal Causality -- 4.3 Proving Generalization -- 5 Cause Synthesis -- 5.1 Proving Our Characterization -- 5.2 Cause-Synthesis Algorithm for -Regular Effects -- 6 Implementation and Evaluation -- 6.1 Cause Synthesis -- 6.2 Cause Checking -- 7 Related Work -- 8 Conclusion -- References -- Dynamic Programming for Symbolic Boolean Realizability and Synthesis -- 1 Introduction -- 2 Preliminary Definitions -- 2.1 Boolean Formula and Synthesis Concepts -- 2.2 Dynamic Programming Concepts - Project-Join Trees -- 3 Realizability CheckingProofs for All Lemmas and Theorems Can Be Found in the Appendix A. -- 3.1 Theoretical Basis and Valuations in Trees -- 3.2 Determining Nullary, Partial and Full Realizability -- 4 Synthesis of Witness Functions -- 4.1 Monolithic Approach -- 4.2 Synthesis Using Graded Project-Join Trees -- 5 Experimental Evaluation -- 5.1 Realizability-Checking Phase -- 5.2 Synthesis -- 5.3 Tree Widths and Realizability -- 5.4 Comparison with Non-BDD-Based Synthesis -- 6 Concluding Remarks -- References -- Localized Attractor Computations for Infinite-State Games -- 1 Introduction -- 2 Preliminaries -- 3 Attractor Computation with Caching -- 4 Abstract Template-Based Cache Generation. 4.1 Generating Attractor Caches from Sub-Games -- 4.2 Constructing Sub-games from Abstract Strategy Templates -- 5 Game Solving with Abstract Template-Based Caching -- 6 Experimental Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Learning -- Bisimulation Learning -- 1 Introduction -- 2 Illustrative Example -- 3 Stutter-Insensitive Bisimulations of Deterministic Transition Systems -- 3.1 Model Checking -- 4 Counterexample-Guided Bisimulation Learning -- 4.1 Learner-Verifier Framework for Bisimulation Learning -- 4.2 Binary Decision Tree Partition Templates -- 5 Experimental Evaluation -- 5.1 Discrete-Time Clock Synchronization -- 5.2 Conditional Termination -- 6 Conclusion -- References -- Regular Reinforcement Learning -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Regular Languages -- 3.2 Rational Transductions -- 3.3 Markov Decision Processes -- 4 Regular Markov Decision Processes -- 4.1 Undecidability of Values -- 4.2 Discounted Optimization -- 4.3 Finiteness Conditions -- 4.4 Q-Learning in RMDPs -- 5 Deep Regular Reinforcement Learning -- 5.1 Token Passing -- 5.2 Duplicating Pebbles -- 5.3 Shunting Yard Algorithm -- 5.4 Modified Tangrams -- 6 Conclusion -- References -- LTL Learning on GPUs -- 1 Introduction -- 2 Formal Preliminaries -- 3 High-Level Structure of the Algorithm -- 4 In-Memory Representation of Search Space -- 5 Correctness and Complexity of the Branch-Free Implementation of Temporal Operators -- 6 Relaxed Uniqueness Checks -- 7 Divide & -- Conquer -- 8 Evaluation of Algorithm Performance -- 9 Conclusion -- References -- Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models -- 1 Introduction -- 2 Problem Setup -- 3 Verified Exploration Through Learned Models -- 3.1 Symbolic Environment Models -- 3.2 Shielding for Verified Safe Exploration. 3.3 Neural Controller Approximation -- 4 Experiments -- 5 Related Work -- 6 Conclusion -- References -- Cyberphysical and Hybrid Systems -- Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems -- 1 Introduction -- 1.1 Related Work -- 1.2 Contributions -- 2 Preliminaries and Problem Statement -- 2.1 Intervals -- 2.2 Truth Values -- 2.3 Signals -- 2.4 Reachability Analysis of Hybrid Systems -- 2.5 Signal Temporal Logic with Boolean Semantics -- 2.6 Problem Statement -- 3 Basic Idea and Solution Concept -- 4 Four-Valued Signal Temporal Logic -- 4.1 Computing Boolean Satisfaction Signals -- 4.2 Computing Three-Valued Satisfaction Signals -- 4.3 Computing Four-Valued Satisfaction Signals -- 5 Incremental Verification of Hybrid Systems -- 5.1 Incremental Verification Algorithm -- 5.2 Refinement via Branching the Reachability Analysis -- 6 Evaluation -- 6.1 Bouncing Ball -- 6.2 Autonomous Driving -- 6.3 Genetic Oscillator -- 7 Conclusion -- References -- Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications -- 1 Introduction -- 2 Preliminaries -- 2.1 Signal Temporal Logic -- 2.2 Finite Variability -- 3 Problem Formulation -- 4 Variable-Interval Encoding of STL to MILP -- 4.1 -Stable Partitions -- 4.2 Variable-Interval MILP Encoding -- 5 System Models and Their MILP Encoding -- 5.1 HAs with Closed-Form Solutions -- 5.2 HAs with Double Integrator Dynamics -- 6 Implementation and Experiments -- References -- Inner-Approximate Reachability Computation via Zonotopic Boundary Analysis -- 1 Introduction -- 2 Preliminaries -- 2.1 Notation -- 2.2 Problem Statement -- 3 Methodology -- 3.1 Inner-Approximation Computation Framework -- 3.2 Extraction of Zonotopes' Boundaries -- 3.3 Zonotopal Tiling and Boundary Refinement -- 3.4 Contracting Computed Outer-Approximation -- 4 Experiments. 4.1 Advantage in Efficiency and Precision -- 4.2 Advantage in Long Time Horizons -- 4.3 Advantage in Big Initial Sets -- 5 Conclusion -- References -- Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs -- 1 Introduction -- 2 Background -- 2.1 Preliminaries -- 2.2 Motivating Example: A Multi-UAV System -- 3 Scenario-Based Formalism for Reconfigurable Systems -- 3.1 Scenario-Based System Modeling -- 3.2 Specifying System Requirements in Topology-Aware STL -- 4 Path-Oriented Optimization-Based System Falsification -- 4.1 Falsification Framework -- 4.2 Path Generation for Hierarchical Scenario Tasks -- 4.3 Optimization-Based Falsification for Paths -- 5 Implementation and Evaluation -- 5.1 Implementation and Research Questions -- 5.2 Experimental Evaluation and Analysis -- 5.3 Threats to Validity -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Probabilistic Systems -- Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games -- 1 Introduction -- 2 Preliminaries -- 3 Complete-Exploration Algorithm for Solving SGs -- 4 Partial-Exploration Algorithm for Solving SGs -- 5 Tool Description -- 6 Experimental Evaluation -- 6.1 Experimental Setup -- 6.2 Results -- 7 Conclusion -- References -- What Should Be Observed for Optimal Reward in POMDPs? -- 1 Introduction -- 2 Preliminaries -- 2.1 Markov Decision Processes (MDPs) -- 2.2 Partially Observable Markov Decision Processes -- 3 The Optimal Observability Problem -- 3.1 Problem Statement -- 3.2 Undecidability -- 4 Optimal Observability for Positional Strategies -- 4.1 Positional and Deterministic Strategies -- 4.2 Positional Randomized Strategies -- 5 Implementation and Experimental Evaluation -- 5.1 Solving Optimal Observability Problems with Parameter Synthesis Tools -- 5.2 Implementation and Setup -- 5.3 Experimental Results. 6 Conclusion and Future Work. |
author_facet |
Gurfinkel, Arie. Ganesh, Vijay. |
author_variant |
a g ag |
author2 |
Ganesh, Vijay. |
author2_variant |
v g vg |
author2_role |
TeilnehmendeR |
author_sort |
Gurfinkel, Arie. |
title |
Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. |
title_sub |
36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. |
title_full |
Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. |
title_fullStr |
Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. |
title_full_unstemmed |
Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. |
title_auth |
Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. |
title_new |
Computer Aided Verification : |
title_sort |
computer aided verification : 36th international conference, cav 2024, montreal, qc, canada, july 24-27, 2024, proceedings, part iii. |
series |
Lecture Notes in Computer Science Series ; |
series2 |
Lecture Notes in Computer Science Series ; |
publisher |
Springer International Publishing AG, |
publishDate |
2024 |
physical |
1 online resource (597 pages) |
edition |
1st ed. |
contents |
Intro -- Preface -- Organization -- Invited Talks -- How to Solve Math Problems Without Talent -- Bridging Formal Mathematics and Software Verification -- The Art of SMT Solving -- Contents - Part III -- Synthesis and Repair -- Syntax-Guided Automated Program Repair for Hyperproperties -- 1 Introduction -- 2 Preliminaries -- 3 Program Repair by Symbolic Execution -- 3.1 Symbolic Execution -- 3.2 Symbolic Paths and Safety Automata -- 3.3 Encoding for HyperLTL -- 3.4 Program Repair Using SyGuS -- 4 Transparent Repair -- 4.1 Transparency -- 4.2 Encoding for Transparent Repair -- 5 Iterative Repair -- 5.1 Encoding for Iterative Repair -- 5.2 Iterative Repair Loop -- 6 Implementation and Evaluation -- 6.1 Iterative Repair for Hyperproperties -- 6.2 Scalability in Solution Size -- 6.3 Evaluation on k-Safety Instances -- 6.4 Evaluation on Functional Properties -- 7 Related Work -- 8 Conclusion -- References -- The SemGuS Toolkit -- 1 Introduction -- 2 The SemGuS Format 1.0 -- 3 A Baseline SemGuS Solver -- 3.1 Verifying Candidate Solutions -- 3.2 Baseline Enumerative Solvers -- 3.3 Extensibility -- 4 Benchmarks and Performance of Baseline Solvers -- 5 Related Work -- References -- Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries -- 4 Constraint Annotated Tree Automata -- 4.1 CATA Operations for Synthesis -- 5 Synthesis Algorithm -- 5.1 Problem Statement -- 5.2 Basic Synthesis Algorithm -- 5.3 Lazy Synthesis Algorithm -- 6 Implementation -- 7 Evaluation -- 8 Related Work -- 9 Conclusion -- References -- Information Flow Guided Synthesis with Unbounded Communication -- 1 Introduction -- 2 Running Example: Sequence Transmission -- 3 Preliminaries -- 4 Prefix Information Flow -- 5 Unbounded Communication in Distributed Systems -- 5.1 Receiving Information. 5.2 Transmitting Information -- 5.3 Safety Hyper Implementations -- 6 Synthesis with Prefix Information Flow Assumptions -- 6.1 Automata for Assume and Guarantee Specifications -- 6.2 Compositional Synthesis -- 7 Experiments -- 8 Related Work -- 9 Conclusion -- References -- Synthesis of Temporal Causality -- 1 Introduction -- 1.1 Temporal Causality -- 1.2 Contributions and Structure -- 2 Preliminaries -- 3 Overview: The Topology of Causality -- 3.1 Actual Causes as Downward Closed Sets of Traces -- 3.2 Causality Without the Limit Assumption -- 4 Generalized Temporal Causality -- 4.1 Similarity Relations and the Limit Assumption -- 4.2 A General Definition of Temporal Causality -- 4.3 Proving Generalization -- 5 Cause Synthesis -- 5.1 Proving Our Characterization -- 5.2 Cause-Synthesis Algorithm for -Regular Effects -- 6 Implementation and Evaluation -- 6.1 Cause Synthesis -- 6.2 Cause Checking -- 7 Related Work -- 8 Conclusion -- References -- Dynamic Programming for Symbolic Boolean Realizability and Synthesis -- 1 Introduction -- 2 Preliminary Definitions -- 2.1 Boolean Formula and Synthesis Concepts -- 2.2 Dynamic Programming Concepts - Project-Join Trees -- 3 Realizability CheckingProofs for All Lemmas and Theorems Can Be Found in the Appendix A. -- 3.1 Theoretical Basis and Valuations in Trees -- 3.2 Determining Nullary, Partial and Full Realizability -- 4 Synthesis of Witness Functions -- 4.1 Monolithic Approach -- 4.2 Synthesis Using Graded Project-Join Trees -- 5 Experimental Evaluation -- 5.1 Realizability-Checking Phase -- 5.2 Synthesis -- 5.3 Tree Widths and Realizability -- 5.4 Comparison with Non-BDD-Based Synthesis -- 6 Concluding Remarks -- References -- Localized Attractor Computations for Infinite-State Games -- 1 Introduction -- 2 Preliminaries -- 3 Attractor Computation with Caching -- 4 Abstract Template-Based Cache Generation. 4.1 Generating Attractor Caches from Sub-Games -- 4.2 Constructing Sub-games from Abstract Strategy Templates -- 5 Game Solving with Abstract Template-Based Caching -- 6 Experimental Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Learning -- Bisimulation Learning -- 1 Introduction -- 2 Illustrative Example -- 3 Stutter-Insensitive Bisimulations of Deterministic Transition Systems -- 3.1 Model Checking -- 4 Counterexample-Guided Bisimulation Learning -- 4.1 Learner-Verifier Framework for Bisimulation Learning -- 4.2 Binary Decision Tree Partition Templates -- 5 Experimental Evaluation -- 5.1 Discrete-Time Clock Synchronization -- 5.2 Conditional Termination -- 6 Conclusion -- References -- Regular Reinforcement Learning -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Regular Languages -- 3.2 Rational Transductions -- 3.3 Markov Decision Processes -- 4 Regular Markov Decision Processes -- 4.1 Undecidability of Values -- 4.2 Discounted Optimization -- 4.3 Finiteness Conditions -- 4.4 Q-Learning in RMDPs -- 5 Deep Regular Reinforcement Learning -- 5.1 Token Passing -- 5.2 Duplicating Pebbles -- 5.3 Shunting Yard Algorithm -- 5.4 Modified Tangrams -- 6 Conclusion -- References -- LTL Learning on GPUs -- 1 Introduction -- 2 Formal Preliminaries -- 3 High-Level Structure of the Algorithm -- 4 In-Memory Representation of Search Space -- 5 Correctness and Complexity of the Branch-Free Implementation of Temporal Operators -- 6 Relaxed Uniqueness Checks -- 7 Divide & -- Conquer -- 8 Evaluation of Algorithm Performance -- 9 Conclusion -- References -- Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models -- 1 Introduction -- 2 Problem Setup -- 3 Verified Exploration Through Learned Models -- 3.1 Symbolic Environment Models -- 3.2 Shielding for Verified Safe Exploration. 3.3 Neural Controller Approximation -- 4 Experiments -- 5 Related Work -- 6 Conclusion -- References -- Cyberphysical and Hybrid Systems -- Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems -- 1 Introduction -- 1.1 Related Work -- 1.2 Contributions -- 2 Preliminaries and Problem Statement -- 2.1 Intervals -- 2.2 Truth Values -- 2.3 Signals -- 2.4 Reachability Analysis of Hybrid Systems -- 2.5 Signal Temporal Logic with Boolean Semantics -- 2.6 Problem Statement -- 3 Basic Idea and Solution Concept -- 4 Four-Valued Signal Temporal Logic -- 4.1 Computing Boolean Satisfaction Signals -- 4.2 Computing Three-Valued Satisfaction Signals -- 4.3 Computing Four-Valued Satisfaction Signals -- 5 Incremental Verification of Hybrid Systems -- 5.1 Incremental Verification Algorithm -- 5.2 Refinement via Branching the Reachability Analysis -- 6 Evaluation -- 6.1 Bouncing Ball -- 6.2 Autonomous Driving -- 6.3 Genetic Oscillator -- 7 Conclusion -- References -- Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications -- 1 Introduction -- 2 Preliminaries -- 2.1 Signal Temporal Logic -- 2.2 Finite Variability -- 3 Problem Formulation -- 4 Variable-Interval Encoding of STL to MILP -- 4.1 -Stable Partitions -- 4.2 Variable-Interval MILP Encoding -- 5 System Models and Their MILP Encoding -- 5.1 HAs with Closed-Form Solutions -- 5.2 HAs with Double Integrator Dynamics -- 6 Implementation and Experiments -- References -- Inner-Approximate Reachability Computation via Zonotopic Boundary Analysis -- 1 Introduction -- 2 Preliminaries -- 2.1 Notation -- 2.2 Problem Statement -- 3 Methodology -- 3.1 Inner-Approximation Computation Framework -- 3.2 Extraction of Zonotopes' Boundaries -- 3.3 Zonotopal Tiling and Boundary Refinement -- 3.4 Contracting Computed Outer-Approximation -- 4 Experiments. 4.1 Advantage in Efficiency and Precision -- 4.2 Advantage in Long Time Horizons -- 4.3 Advantage in Big Initial Sets -- 5 Conclusion -- References -- Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs -- 1 Introduction -- 2 Background -- 2.1 Preliminaries -- 2.2 Motivating Example: A Multi-UAV System -- 3 Scenario-Based Formalism for Reconfigurable Systems -- 3.1 Scenario-Based System Modeling -- 3.2 Specifying System Requirements in Topology-Aware STL -- 4 Path-Oriented Optimization-Based System Falsification -- 4.1 Falsification Framework -- 4.2 Path Generation for Hierarchical Scenario Tasks -- 4.3 Optimization-Based Falsification for Paths -- 5 Implementation and Evaluation -- 5.1 Implementation and Research Questions -- 5.2 Experimental Evaluation and Analysis -- 5.3 Threats to Validity -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Probabilistic Systems -- Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games -- 1 Introduction -- 2 Preliminaries -- 3 Complete-Exploration Algorithm for Solving SGs -- 4 Partial-Exploration Algorithm for Solving SGs -- 5 Tool Description -- 6 Experimental Evaluation -- 6.1 Experimental Setup -- 6.2 Results -- 7 Conclusion -- References -- What Should Be Observed for Optimal Reward in POMDPs? -- 1 Introduction -- 2 Preliminaries -- 2.1 Markov Decision Processes (MDPs) -- 2.2 Partially Observable Markov Decision Processes -- 3 The Optimal Observability Problem -- 3.1 Problem Statement -- 3.2 Undecidability -- 4 Optimal Observability for Positional Strategies -- 4.1 Positional and Deterministic Strategies -- 4.2 Positional Randomized Strategies -- 5 Implementation and Experimental Evaluation -- 5.1 Solving Optimal Observability Problems with Parameter Synthesis Tools -- 5.2 Implementation and Setup -- 5.3 Experimental Results. 6 Conclusion and Future Work. |
isbn |
3-031-65633-4 3-031-65632-6 |
callnumber-first |
Q - Science |
callnumber-subject |
QA - Mathematics |
callnumber-label |
QA76 |
callnumber-sort |
QA 276.758 |
illustrated |
Not Illustrated |
work_keys_str_mv |
AT gurfinkelarie computeraidedverification36thinternationalconferencecav2024montrealqccanadajuly24272024proceedingspartiii AT ganeshvijay computeraidedverification36thinternationalconferencecav2024montrealqccanadajuly24272024proceedingspartiii |
status_str |
n |
ids_txt_mv |
(CKB)33600912200041 (MiAaPQ)EBC31594174 (Au-PeEL)EBL31594174 (EXLCZ)9933600912200041 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Lecture Notes in Computer Science Series ; v.14683 |
is_hierarchy_title |
Computer Aided Verification : 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. |
container_title |
Lecture Notes in Computer Science Series ; v.14683 |
author2_original_writing_str_mv |
noLinkedField |
_version_ |
1809671915396136960 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>11132nam a22004573i 4500</leader><controlfield tag="001">993687476404498</controlfield><controlfield tag="005">20240812084530.0</controlfield><controlfield tag="006">m o d | </controlfield><controlfield tag="007">cr |||||||||||</controlfield><controlfield tag="008">240812s2024 xx o ||||0 eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">3-031-65633-4</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(CKB)33600912200041</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(MiAaPQ)EBC31594174</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(Au-PeEL)EBL31594174</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(EXLCZ)9933600912200041</subfield></datafield><datafield tag="040" ind1=" " ind2=" "><subfield code="a">MiAaPQ</subfield><subfield code="b">eng</subfield><subfield code="e">rda</subfield><subfield code="e">pn</subfield><subfield code="c">MiAaPQ</subfield><subfield code="d">MiAaPQ</subfield></datafield><datafield tag="050" ind1=" " ind2="4"><subfield code="a">QA76.758</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Gurfinkel, Arie.</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Computer Aided Verification :</subfield><subfield code="b">36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III.</subfield></datafield><datafield tag="250" ind1=" " ind2=" "><subfield code="a">1st ed.</subfield></datafield><datafield tag="264" ind1=" " ind2="1"><subfield code="a">Cham :</subfield><subfield code="b">Springer International Publishing AG,</subfield><subfield code="c">2024.</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">©2024.</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (597 pages)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="490" ind1="1" ind2=" "><subfield code="a">Lecture Notes in Computer Science Series ;</subfield><subfield code="v">v.14683</subfield></datafield><datafield tag="588" ind1=" " ind2=" "><subfield code="a">Description based on publisher supplied metadata and other sources.</subfield></datafield><datafield tag="505" ind1="0" ind2=" "><subfield code="a">Intro -- Preface -- Organization -- Invited Talks -- How to Solve Math Problems Without Talent -- Bridging Formal Mathematics and Software Verification -- The Art of SMT Solving -- Contents - Part III -- Synthesis and Repair -- Syntax-Guided Automated Program Repair for Hyperproperties -- 1 Introduction -- 2 Preliminaries -- 3 Program Repair by Symbolic Execution -- 3.1 Symbolic Execution -- 3.2 Symbolic Paths and Safety Automata -- 3.3 Encoding for HyperLTL -- 3.4 Program Repair Using SyGuS -- 4 Transparent Repair -- 4.1 Transparency -- 4.2 Encoding for Transparent Repair -- 5 Iterative Repair -- 5.1 Encoding for Iterative Repair -- 5.2 Iterative Repair Loop -- 6 Implementation and Evaluation -- 6.1 Iterative Repair for Hyperproperties -- 6.2 Scalability in Solution Size -- 6.3 Evaluation on k-Safety Instances -- 6.4 Evaluation on Functional Properties -- 7 Related Work -- 8 Conclusion -- References -- The SemGuS Toolkit -- 1 Introduction -- 2 The SemGuS Format 1.0 -- 3 A Baseline SemGuS Solver -- 3.1 Verifying Candidate Solutions -- 3.2 Baseline Enumerative Solvers -- 3.3 Extensibility -- 4 Benchmarks and Performance of Baseline Solvers -- 5 Related Work -- References -- Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries -- 4 Constraint Annotated Tree Automata -- 4.1 CATA Operations for Synthesis -- 5 Synthesis Algorithm -- 5.1 Problem Statement -- 5.2 Basic Synthesis Algorithm -- 5.3 Lazy Synthesis Algorithm -- 6 Implementation -- 7 Evaluation -- 8 Related Work -- 9 Conclusion -- References -- Information Flow Guided Synthesis with Unbounded Communication -- 1 Introduction -- 2 Running Example: Sequence Transmission -- 3 Preliminaries -- 4 Prefix Information Flow -- 5 Unbounded Communication in Distributed Systems -- 5.1 Receiving Information.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">5.2 Transmitting Information -- 5.3 Safety Hyper Implementations -- 6 Synthesis with Prefix Information Flow Assumptions -- 6.1 Automata for Assume and Guarantee Specifications -- 6.2 Compositional Synthesis -- 7 Experiments -- 8 Related Work -- 9 Conclusion -- References -- Synthesis of Temporal Causality -- 1 Introduction -- 1.1 Temporal Causality -- 1.2 Contributions and Structure -- 2 Preliminaries -- 3 Overview: The Topology of Causality -- 3.1 Actual Causes as Downward Closed Sets of Traces -- 3.2 Causality Without the Limit Assumption -- 4 Generalized Temporal Causality -- 4.1 Similarity Relations and the Limit Assumption -- 4.2 A General Definition of Temporal Causality -- 4.3 Proving Generalization -- 5 Cause Synthesis -- 5.1 Proving Our Characterization -- 5.2 Cause-Synthesis Algorithm for -Regular Effects -- 6 Implementation and Evaluation -- 6.1 Cause Synthesis -- 6.2 Cause Checking -- 7 Related Work -- 8 Conclusion -- References -- Dynamic Programming for Symbolic Boolean Realizability and Synthesis -- 1 Introduction -- 2 Preliminary Definitions -- 2.1 Boolean Formula and Synthesis Concepts -- 2.2 Dynamic Programming Concepts - Project-Join Trees -- 3 Realizability CheckingProofs for All Lemmas and Theorems Can Be Found in the Appendix A. -- 3.1 Theoretical Basis and Valuations in Trees -- 3.2 Determining Nullary, Partial and Full Realizability -- 4 Synthesis of Witness Functions -- 4.1 Monolithic Approach -- 4.2 Synthesis Using Graded Project-Join Trees -- 5 Experimental Evaluation -- 5.1 Realizability-Checking Phase -- 5.2 Synthesis -- 5.3 Tree Widths and Realizability -- 5.4 Comparison with Non-BDD-Based Synthesis -- 6 Concluding Remarks -- References -- Localized Attractor Computations for Infinite-State Games -- 1 Introduction -- 2 Preliminaries -- 3 Attractor Computation with Caching -- 4 Abstract Template-Based Cache Generation.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4.1 Generating Attractor Caches from Sub-Games -- 4.2 Constructing Sub-games from Abstract Strategy Templates -- 5 Game Solving with Abstract Template-Based Caching -- 6 Experimental Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Learning -- Bisimulation Learning -- 1 Introduction -- 2 Illustrative Example -- 3 Stutter-Insensitive Bisimulations of Deterministic Transition Systems -- 3.1 Model Checking -- 4 Counterexample-Guided Bisimulation Learning -- 4.1 Learner-Verifier Framework for Bisimulation Learning -- 4.2 Binary Decision Tree Partition Templates -- 5 Experimental Evaluation -- 5.1 Discrete-Time Clock Synchronization -- 5.2 Conditional Termination -- 6 Conclusion -- References -- Regular Reinforcement Learning -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Regular Languages -- 3.2 Rational Transductions -- 3.3 Markov Decision Processes -- 4 Regular Markov Decision Processes -- 4.1 Undecidability of Values -- 4.2 Discounted Optimization -- 4.3 Finiteness Conditions -- 4.4 Q-Learning in RMDPs -- 5 Deep Regular Reinforcement Learning -- 5.1 Token Passing -- 5.2 Duplicating Pebbles -- 5.3 Shunting Yard Algorithm -- 5.4 Modified Tangrams -- 6 Conclusion -- References -- LTL Learning on GPUs -- 1 Introduction -- 2 Formal Preliminaries -- 3 High-Level Structure of the Algorithm -- 4 In-Memory Representation of Search Space -- 5 Correctness and Complexity of the Branch-Free Implementation of Temporal Operators -- 6 Relaxed Uniqueness Checks -- 7 Divide &amp -- Conquer -- 8 Evaluation of Algorithm Performance -- 9 Conclusion -- References -- Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models -- 1 Introduction -- 2 Problem Setup -- 3 Verified Exploration Through Learned Models -- 3.1 Symbolic Environment Models -- 3.2 Shielding for Verified Safe Exploration.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">3.3 Neural Controller Approximation -- 4 Experiments -- 5 Related Work -- 6 Conclusion -- References -- Cyberphysical and Hybrid Systems -- Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems -- 1 Introduction -- 1.1 Related Work -- 1.2 Contributions -- 2 Preliminaries and Problem Statement -- 2.1 Intervals -- 2.2 Truth Values -- 2.3 Signals -- 2.4 Reachability Analysis of Hybrid Systems -- 2.5 Signal Temporal Logic with Boolean Semantics -- 2.6 Problem Statement -- 3 Basic Idea and Solution Concept -- 4 Four-Valued Signal Temporal Logic -- 4.1 Computing Boolean Satisfaction Signals -- 4.2 Computing Three-Valued Satisfaction Signals -- 4.3 Computing Four-Valued Satisfaction Signals -- 5 Incremental Verification of Hybrid Systems -- 5.1 Incremental Verification Algorithm -- 5.2 Refinement via Branching the Reachability Analysis -- 6 Evaluation -- 6.1 Bouncing Ball -- 6.2 Autonomous Driving -- 6.3 Genetic Oscillator -- 7 Conclusion -- References -- Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications -- 1 Introduction -- 2 Preliminaries -- 2.1 Signal Temporal Logic -- 2.2 Finite Variability -- 3 Problem Formulation -- 4 Variable-Interval Encoding of STL to MILP -- 4.1 -Stable Partitions -- 4.2 Variable-Interval MILP Encoding -- 5 System Models and Their MILP Encoding -- 5.1 HAs with Closed-Form Solutions -- 5.2 HAs with Double Integrator Dynamics -- 6 Implementation and Experiments -- References -- Inner-Approximate Reachability Computation via Zonotopic Boundary Analysis -- 1 Introduction -- 2 Preliminaries -- 2.1 Notation -- 2.2 Problem Statement -- 3 Methodology -- 3.1 Inner-Approximation Computation Framework -- 3.2 Extraction of Zonotopes' Boundaries -- 3.3 Zonotopal Tiling and Boundary Refinement -- 3.4 Contracting Computed Outer-Approximation -- 4 Experiments.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4.1 Advantage in Efficiency and Precision -- 4.2 Advantage in Long Time Horizons -- 4.3 Advantage in Big Initial Sets -- 5 Conclusion -- References -- Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs -- 1 Introduction -- 2 Background -- 2.1 Preliminaries -- 2.2 Motivating Example: A Multi-UAV System -- 3 Scenario-Based Formalism for Reconfigurable Systems -- 3.1 Scenario-Based System Modeling -- 3.2 Specifying System Requirements in Topology-Aware STL -- 4 Path-Oriented Optimization-Based System Falsification -- 4.1 Falsification Framework -- 4.2 Path Generation for Hierarchical Scenario Tasks -- 4.3 Optimization-Based Falsification for Paths -- 5 Implementation and Evaluation -- 5.1 Implementation and Research Questions -- 5.2 Experimental Evaluation and Analysis -- 5.3 Threats to Validity -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Probabilistic Systems -- Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games -- 1 Introduction -- 2 Preliminaries -- 3 Complete-Exploration Algorithm for Solving SGs -- 4 Partial-Exploration Algorithm for Solving SGs -- 5 Tool Description -- 6 Experimental Evaluation -- 6.1 Experimental Setup -- 6.2 Results -- 7 Conclusion -- References -- What Should Be Observed for Optimal Reward in POMDPs? -- 1 Introduction -- 2 Preliminaries -- 2.1 Markov Decision Processes (MDPs) -- 2.2 Partially Observable Markov Decision Processes -- 3 The Optimal Observability Problem -- 3.1 Problem Statement -- 3.2 Undecidability -- 4 Optimal Observability for Positional Strategies -- 4.1 Positional and Deterministic Strategies -- 4.2 Positional Randomized Strategies -- 5 Implementation and Experimental Evaluation -- 5.1 Solving Optimal Observability Problems with Parameter Synthesis Tools -- 5.2 Implementation and Setup -- 5.3 Experimental Results.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">6 Conclusion and Future Work.</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Ganesh, Vijay.</subfield></datafield><datafield tag="776" ind1=" " ind2=" "><subfield code="z">3-031-65632-6</subfield></datafield><datafield tag="830" ind1=" " ind2="0"><subfield code="a">Lecture Notes in Computer Science Series</subfield></datafield><datafield tag="906" ind1=" " ind2=" "><subfield code="a">BOOK</subfield></datafield><datafield tag="ADM" ind1=" " ind2=" "><subfield code="b">2024-09-09 00:20:38 Europe/Vienna</subfield><subfield code="f">System</subfield><subfield code="c">marc21</subfield><subfield code="a">2024-08-04 11:53:48 Europe/Vienna</subfield><subfield code="g">false</subfield></datafield><datafield tag="AVE" ind1=" " ind2=" "><subfield code="i">DOAB Directory of Open Access Books</subfield><subfield code="P">DOAB Directory of Open Access Books</subfield><subfield code="x">https://eu02.alma.exlibrisgroup.com/view/uresolver/43ACC_OEAW/openurl?u.ignore_date_coverage=true&portfolio_pid=5357522710004498&Force_direct=true</subfield><subfield code="Z">5357522710004498</subfield><subfield code="b">Available</subfield><subfield code="8">5357522710004498</subfield></datafield></record></collection> |