Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Automated reasoning with analytic tableaux and related methods : International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, May 5-8, 1998 : proceedings / / Harrie de Swart (editor)
| Automated reasoning with analytic tableaux and related methods : International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, May 5-8, 1998 : proceedings / / Harrie de Swart (editor) |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin : , : Springer, , [1998] |
| Descrizione fisica | 1 online resource (X, 325 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Automatic theorem proving
Artificial intelligence |
| ISBN | 3-540-69778-0 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Extended Abstracts of Invited Lectures -- Philosophical Aspects of Computerized Verification of Mathematics -- A Science of Reasoning (Extended Abstract) -- Model Checking: Historical Perspective and Example (Extended Abstract) -- Comparison -- Comparison of Theorem Provers for Modal Logics — Introduction and Summary -- FaCT and DLP -- Prover KT4 -- leanK 2.0 -- Logics Workbench 1.0 -- Optimised Functional Translation and Resolution -- Benchmark Evaluation of ?KE -- Abstracts of the Tutorials -- Implementation of Propositional Temporal Logics Using BDDs -- Computer Programming as Mathematics in a Programming Language and Proof System CL -- Contributed Research Papers -- A Tableau Calculus for Multimodal Logics and Some (Un)Decidability Results -- Hyper Tableau — The Next Generation -- Fibring Semantic Tableaux -- A Tableau Calculus for Quantifier-Free Set Theoretic Formulae -- A Tableau Method for Interval Temporal Logic with Projection -- Bounded Model Search in Linear Temporal Logic and Its Application to Planning -- On Proof Complexity of Circumscription -- Tableaux for Finite-Valued Logics with Arbitrary Distribution Modalities -- Some Remarks on Completeness, Connection Graph Resolution, and Link Deletion -- Simplification and Backjumping in Modal Tableau -- Free Variable Tableaux for a Logic with Term Declarations -- Simplification A General Constraint Propagation Technique for Propositional and Modal Tableaux -- A Tableaux Calculus for Ambiguous Quantifiation -- From Kripke Models to Algebraic Counter-Valuations -- Deleting Redundancy in Proof Reconstruction -- A New One-Pass Tableau Calculus for PLTL -- Decision Procedures for Intuitionistic Propositional Logic by Program Extraction -- Contributed System Descriptions -- The FaCT System -- Implementation of Proof Search in the Imperative Programming Language Pizza -- p-SETHEO: Strategy Parallelism in Automated Theorem Proving. |
| Record Nr. | UNISA-996466109103316 |
| Berlin : , : Springer, , [1998] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated technology for verification and analysis : 20th International Symposium, ATVA 2022, Beijing, China, October 25-28, 2022, proceedings / / edited by Ahmed Bouajjani, Lukás Holík, and Zhilin Wu
| Automated technology for verification and analysis : 20th International Symposium, ATVA 2022, Beijing, China, October 25-28, 2022, proceedings / / edited by Ahmed Bouajjani, Lukás Holík, and Zhilin Wu |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (442 pages) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-031-19992-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Abstracts of Invited Talks -- Compositional Reasoning about Concurrent Randomized Programs (Extended Abstract) -- Flattening String Constraints -- Runtime Assurance for Verified AI-Based Autonomy -- The Civl Verifier -- Subgame Perfect Equilibrium with an Algorithmic Perspective -- Contents -- Invited Paper -- Learning Monitorable Operational Design Domains for Assured Autonomy -- 1 Introduction -- 2 Motivating Example: Autonomous Lane Keeping -- 3 Optimal Monitors for Operational Design Domains -- 3.1 Learning Monitors for ODDs -- 3.2 Challenges in Learning Monitorable ODDs -- 3.3 Quantitative Monitor Learning -- 3.4 Black-Box vs. White-Box Settings -- 4 Framework -- 4.1 Main Workflow -- 4.2 Simulation-Based Analysis Using VerifAI and Scenic -- 4.3 Data Generation -- 4.4 Conformance Testing -- 5 Experiments -- 5.1 Experimental Setup -- 5.2 Results -- 6 Related Work -- 7 Conclusion -- References -- Reinforcement Learning -- Dynamic Shielding for Reinforcement Learning in Black-Box Environments -- 1 Introduction -- 1.1 Related Works -- 2 Preliminaries -- 2.1 Automata and Games for System Modeling -- 2.2 Safety Automata for Specifications -- 2.3 Shielding for Safe Reinforcement Learning -- 2.4 The RPNI Algorithm for Passive Automata Learning -- 3 Dynamic Shielding with Online Automata Inference -- 3.1 Dynamic Shielding Scheme -- 3.2 Challenge 1: Incompleteness of the Learned FSRS -- 3.3 Challenge 2: Precision in Automata Learning -- 3.4 Theoretical Validity of Our Dynamic Shielding -- 4 Experimental Evaluation -- 4.1 Implementation and Experiments -- 4.2 Benchmarks -- 4.3 RQ1: Safety by Dynamic Shielding in the Training Phase -- 4.4 RQ2: Performance of the Resulting Controller -- 4.5 RQ3: Time Efficiency of Dynamic Shielding -- 5 Conclusions and Perspectives -- References.
An Impossibility Result in Automata-Theoretic Reinforcement Learning -- 1 Introduction -- 2 Omega-Automata -- 3 Closure Properties of Acceptance Conditions -- 4 Markov Decision Processes -- 4.1 Optimal Strategies Against Omega-Automata -- 4.2 Optimal Strategies Against Scalar Rewards -- 5 Memoryless Reward Translations for RL -- 5.1 Memoryless Reward Translation -- 5.2 Conditions for Memoryless Reductions -- 6 Conclusion -- References -- Reusable Contracts for Safe Integration of Reinforcement Learning in Hybrid Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Reinforcement Learning -- 2.2 Simulink and the RL Toolbox -- 2.3 Deductive Verification with the Differential Dynamic Logic -- 2.4 Transformation from Simulink to dL -- 3 Related Work -- 4 Reusable Hybrid Contracts -- 4.1 Illustrating Examples -- 4.2 Recurring Elements -- 4.3 Threshold Pattern -- 4.4 Range Pattern -- 4.5 Range Recovery Pattern -- 4.6 Resilience Contracts -- 4.7 Deductive Verification in KeYmaera X -- 5 Conclusion -- References -- Program Analysis and Verification -- SISL: Concolic Testing of Structured Binary Input Formats via Partial Specification -- 1 Introduction -- 2 Scheme-Based Input Specification Language -- 3 Overview and Implementation -- 4 Experiments and Conclusion -- References -- Fence Synthesis Under the C11 Memory Model -- 1 Introduction -- 2 Overview of FenSying and fFenSying -- 3 Preliminaries -- 4 Background: C11 Memory Model -- 5 Invalidating Buggy Traces with C11 Fences -- 6 Methodology -- 7 Implementation and Results -- 8 Related Work -- 9 Conclusion and Future Work -- References -- Checking Scheduling-Induced Violations of Control Safety Properties -- 1 Introduction -- 2 System Model and Encoding -- 2.1 Control System Model and Evolution -- 2.2 Task Specification -- 2.3 An Abstraction for Task Runs -- 2.4 Control Action Update Modeling. 2.5 Composing Control and Scheduling Models -- 3 Refining the Abstraction -- 3.1 Overlapping Jobs -- 3.2 Schedule Violation -- 3.3 Work Conservation Violation -- 3.4 Unconstrained Control Updates -- 3.5 Correctness of Refinement -- 4 Tool Design -- 5 Case Study 1: DC Motor Control Model -- 6 Case Study 2: RC Network Control Model -- 7 Case Study 3: F1Tenth Car Model -- 8 Conclusions and Future Work -- References -- Symbolic Runtime Verification for Monitoring Under Uncertainties and Assumptions -- 1 Introduction -- 2 Preliminaries -- 3 A Framework for Symbolic Runtime Verification -- 3.1 Symbolic Expressions -- 3.2 Symbolic Monitor Semantics -- 3.3 A Symbolic Runtime Verification Algorithm -- 4 Symbolic Runtime Verification at Work -- 4.1 Application to Lola Fragments -- 4.2 Temporal Assumptions -- 5 Implementation and Empirical Evaluation -- 6 Conclusion -- References -- SMT and Verification -- Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test -- 1 Introduction -- 2 Background -- 2.1 Unconstrained Global Optimisation -- 2.2 Interval Arithmetic -- 2.3 Robustness and Quasi-decidability -- 2.4 Topological Degree Test -- 3 Local Search Using Unconstrained Global Optimisation -- 4 Solving Bounded Instances with the Topological Degree Test and Interval Arithmetic -- 4.1 Quasi-decidability Procedure -- 4.2 From a Formula with nm to Quasi-dec -- 4.3 A General Procedure -- 5 From Constraint Sets to Formulas -- 5.1 An Eager Approach -- 5.2 A Lazy Approach -- 6 Experimental Evaluation -- 7 Conclusions and Future Work -- References -- Verification of SMT Systems with Quantifiers -- 1 Introduction -- 2 Preliminaries -- 3 Verification of Quantified SMT Systems -- 3.1 Symbolic Formalism -- 3.2 Overview -- 3.3 Ground Instances -- 3.4 Generalizing Invariants from Instances -- 3.5 Invariant Checking. 3.6 Termination -- 4 Related Work -- 5 Experimental Evaluation -- 6 Conclusions and Future Work -- References -- Projected Model Counting: Beyond Independent Support -- 1 Introduction -- 2 Notation and Preliminaries -- 3 Related Work -- 4 Technical Contribution -- 4.1 Extremal Properties of GIS and UBS -- 4.2 Algorithm to Compute Projected Count Using UBS -- 5 Experimental Evaluation -- 6 Conclusion -- References -- Automata and Applications -- Minimization of Automata for Liveness Languages -- 1 Introduction -- 2 Preliminaries -- 2.1 Automata -- 2.2 Liveness Languages -- 2.3 Graphs, Nice Graphs, and the Vertex-Cover Problem -- 3 Live1 Languages -- 3.1 Minimizing Automata for Live1 and Doom1 Languages -- 4 Live2 Languages -- 4.1 Minimizing DBWs and GFG-NBWs for Live2 Languages -- 4.2 Minimizing DCWs and GFG-NCWs for Doom2 Languages -- 4.3 Minimizing Automata with Transition-Based Acceptance for Live2 Languages -- 5 Live3 Languages -- References -- Temporal Causality in Reactive Systems -- 1 Introduction -- 2 Preliminaries -- 3 Motivating Example -- 4 Property Causality -- 4.1 Interventions -- 4.2 Contingencies -- 4.3 Actual Causality for Trace Properties -- 5 Checking -Regular Causality -- 5.1 Interventions -- 5.2 Contingencies -- 5.3 Minimality -- 5.4 Deciding -Regular Causality -- 6 Related Work -- 7 Conclusion -- References -- PDAAAL: A Library for Reachability Analysis of Weighted Pushdown Systems -- 1 Introduction -- 2 Weighted Pushdown Systems and Reachability -- 3 Implemented Algorithms and PDAAAL Architecture -- 4 Comparison with State-of-the-Art -- 5 Applications -- 6 Conclusion -- References -- Active Learning -- Learning Deterministic One-Clock Timed Automata via Mutation Testing -- 1 Introduction -- 2 Preliminaries -- 2.1 Deterministic One-Clock Timed Automata -- 2.2 Active Learning Algorithm for DOTAs -- 2.3 Model-Based Mutation Testing. 3 Mutation-Based Testing for DOTAs -- 3.1 The Process Overview -- 3.2 Heuristic Test-Case Generation -- 3.3 Mutation and Score-Based Test-Case Selection -- 4 Learning-Friendly Mutation Operators for DOTAs -- 4.1 Timed Mutation Operator -- 4.2 Split-Location Mutation Operator -- 5 Implementation and Experiments -- 5.1 Case Studies -- 5.2 Evaluation of Improvements -- 6 Conclusion -- References -- Active Learning of One-Clock Timed Automata Using Constraint Solving -- 1 Introduction -- 2 Preliminaries -- 3 Learning Algorithm -- 3.1 Alignment and Comparison of Timed Words -- 3.2 Timed Observation Table -- 3.3 Encoding of Readiness Constraints -- 3.4 Hypothesis Construction -- 3.5 Main Algorithm and Correctness -- 4 Extension to Deterministic Timed Mealy Machines -- 5 Implementation and Experiments -- 5.1 Experiments on DOTAs -- 5.2 Experiments on TMMs -- 6 Conclusion -- References -- Learning and Characterizing Fully-Ordered Lattice Automata -- 1 Introduction -- 2 Preliminaries -- 3 A Myhill-Nerode Characterization for FOLAs -- 3.1 No Unique Minimal FOLA -- 3.2 Difficulties in Defining f -- 3.3 Defining the Equivalence Relation -- 3.4 The Correspondence Between f and a Minimal FOLA -- 4 The Learning Algorithm -- 5 Empirical Results -- 6 Conclusions -- References -- Probabilistic and Stochastic Systems -- Optimistic and Topological Value Iteration for Simple Stochastic Games -- 1 Introduction -- 2 Preliminaries -- 2.1 Simple Stochastic Games -- 2.2 Value Iteration and Bounded Value Iteration -- 3 Optimistic Value Iteration -- 4 Precise Topological Value Iteration -- 5 Random Generation of Simple Stochastic Games -- 6 Experiments -- 6.1 Experimental Setup -- 6.2 Overview -- 6.3 Detailed Analysis of Precise Algorithms -- 6.4 Detailed Analysis of Approximate (-Precise) Algorithms -- 7 Conclusion -- References -- Alternating Good-for-MDPs Automata. 1 Introduction. |
| Record Nr. | UNISA-996495567803316 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated technology for verification and analysis : 20th International Symposium, ATVA 2022, Beijing, China, October 25-28, 2022, proceedings / / edited by Ahmed Bouajjani, Lukás Holík, and Zhilin Wu
| Automated technology for verification and analysis : 20th International Symposium, ATVA 2022, Beijing, China, October 25-28, 2022, proceedings / / edited by Ahmed Bouajjani, Lukás Holík, and Zhilin Wu |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (442 pages) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-031-19992-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Abstracts of Invited Talks -- Compositional Reasoning about Concurrent Randomized Programs (Extended Abstract) -- Flattening String Constraints -- Runtime Assurance for Verified AI-Based Autonomy -- The Civl Verifier -- Subgame Perfect Equilibrium with an Algorithmic Perspective -- Contents -- Invited Paper -- Learning Monitorable Operational Design Domains for Assured Autonomy -- 1 Introduction -- 2 Motivating Example: Autonomous Lane Keeping -- 3 Optimal Monitors for Operational Design Domains -- 3.1 Learning Monitors for ODDs -- 3.2 Challenges in Learning Monitorable ODDs -- 3.3 Quantitative Monitor Learning -- 3.4 Black-Box vs. White-Box Settings -- 4 Framework -- 4.1 Main Workflow -- 4.2 Simulation-Based Analysis Using VerifAI and Scenic -- 4.3 Data Generation -- 4.4 Conformance Testing -- 5 Experiments -- 5.1 Experimental Setup -- 5.2 Results -- 6 Related Work -- 7 Conclusion -- References -- Reinforcement Learning -- Dynamic Shielding for Reinforcement Learning in Black-Box Environments -- 1 Introduction -- 1.1 Related Works -- 2 Preliminaries -- 2.1 Automata and Games for System Modeling -- 2.2 Safety Automata for Specifications -- 2.3 Shielding for Safe Reinforcement Learning -- 2.4 The RPNI Algorithm for Passive Automata Learning -- 3 Dynamic Shielding with Online Automata Inference -- 3.1 Dynamic Shielding Scheme -- 3.2 Challenge 1: Incompleteness of the Learned FSRS -- 3.3 Challenge 2: Precision in Automata Learning -- 3.4 Theoretical Validity of Our Dynamic Shielding -- 4 Experimental Evaluation -- 4.1 Implementation and Experiments -- 4.2 Benchmarks -- 4.3 RQ1: Safety by Dynamic Shielding in the Training Phase -- 4.4 RQ2: Performance of the Resulting Controller -- 4.5 RQ3: Time Efficiency of Dynamic Shielding -- 5 Conclusions and Perspectives -- References.
An Impossibility Result in Automata-Theoretic Reinforcement Learning -- 1 Introduction -- 2 Omega-Automata -- 3 Closure Properties of Acceptance Conditions -- 4 Markov Decision Processes -- 4.1 Optimal Strategies Against Omega-Automata -- 4.2 Optimal Strategies Against Scalar Rewards -- 5 Memoryless Reward Translations for RL -- 5.1 Memoryless Reward Translation -- 5.2 Conditions for Memoryless Reductions -- 6 Conclusion -- References -- Reusable Contracts for Safe Integration of Reinforcement Learning in Hybrid Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Reinforcement Learning -- 2.2 Simulink and the RL Toolbox -- 2.3 Deductive Verification with the Differential Dynamic Logic -- 2.4 Transformation from Simulink to dL -- 3 Related Work -- 4 Reusable Hybrid Contracts -- 4.1 Illustrating Examples -- 4.2 Recurring Elements -- 4.3 Threshold Pattern -- 4.4 Range Pattern -- 4.5 Range Recovery Pattern -- 4.6 Resilience Contracts -- 4.7 Deductive Verification in KeYmaera X -- 5 Conclusion -- References -- Program Analysis and Verification -- SISL: Concolic Testing of Structured Binary Input Formats via Partial Specification -- 1 Introduction -- 2 Scheme-Based Input Specification Language -- 3 Overview and Implementation -- 4 Experiments and Conclusion -- References -- Fence Synthesis Under the C11 Memory Model -- 1 Introduction -- 2 Overview of FenSying and fFenSying -- 3 Preliminaries -- 4 Background: C11 Memory Model -- 5 Invalidating Buggy Traces with C11 Fences -- 6 Methodology -- 7 Implementation and Results -- 8 Related Work -- 9 Conclusion and Future Work -- References -- Checking Scheduling-Induced Violations of Control Safety Properties -- 1 Introduction -- 2 System Model and Encoding -- 2.1 Control System Model and Evolution -- 2.2 Task Specification -- 2.3 An Abstraction for Task Runs -- 2.4 Control Action Update Modeling. 2.5 Composing Control and Scheduling Models -- 3 Refining the Abstraction -- 3.1 Overlapping Jobs -- 3.2 Schedule Violation -- 3.3 Work Conservation Violation -- 3.4 Unconstrained Control Updates -- 3.5 Correctness of Refinement -- 4 Tool Design -- 5 Case Study 1: DC Motor Control Model -- 6 Case Study 2: RC Network Control Model -- 7 Case Study 3: F1Tenth Car Model -- 8 Conclusions and Future Work -- References -- Symbolic Runtime Verification for Monitoring Under Uncertainties and Assumptions -- 1 Introduction -- 2 Preliminaries -- 3 A Framework for Symbolic Runtime Verification -- 3.1 Symbolic Expressions -- 3.2 Symbolic Monitor Semantics -- 3.3 A Symbolic Runtime Verification Algorithm -- 4 Symbolic Runtime Verification at Work -- 4.1 Application to Lola Fragments -- 4.2 Temporal Assumptions -- 5 Implementation and Empirical Evaluation -- 6 Conclusion -- References -- SMT and Verification -- Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test -- 1 Introduction -- 2 Background -- 2.1 Unconstrained Global Optimisation -- 2.2 Interval Arithmetic -- 2.3 Robustness and Quasi-decidability -- 2.4 Topological Degree Test -- 3 Local Search Using Unconstrained Global Optimisation -- 4 Solving Bounded Instances with the Topological Degree Test and Interval Arithmetic -- 4.1 Quasi-decidability Procedure -- 4.2 From a Formula with nm to Quasi-dec -- 4.3 A General Procedure -- 5 From Constraint Sets to Formulas -- 5.1 An Eager Approach -- 5.2 A Lazy Approach -- 6 Experimental Evaluation -- 7 Conclusions and Future Work -- References -- Verification of SMT Systems with Quantifiers -- 1 Introduction -- 2 Preliminaries -- 3 Verification of Quantified SMT Systems -- 3.1 Symbolic Formalism -- 3.2 Overview -- 3.3 Ground Instances -- 3.4 Generalizing Invariants from Instances -- 3.5 Invariant Checking. 3.6 Termination -- 4 Related Work -- 5 Experimental Evaluation -- 6 Conclusions and Future Work -- References -- Projected Model Counting: Beyond Independent Support -- 1 Introduction -- 2 Notation and Preliminaries -- 3 Related Work -- 4 Technical Contribution -- 4.1 Extremal Properties of GIS and UBS -- 4.2 Algorithm to Compute Projected Count Using UBS -- 5 Experimental Evaluation -- 6 Conclusion -- References -- Automata and Applications -- Minimization of Automata for Liveness Languages -- 1 Introduction -- 2 Preliminaries -- 2.1 Automata -- 2.2 Liveness Languages -- 2.3 Graphs, Nice Graphs, and the Vertex-Cover Problem -- 3 Live1 Languages -- 3.1 Minimizing Automata for Live1 and Doom1 Languages -- 4 Live2 Languages -- 4.1 Minimizing DBWs and GFG-NBWs for Live2 Languages -- 4.2 Minimizing DCWs and GFG-NCWs for Doom2 Languages -- 4.3 Minimizing Automata with Transition-Based Acceptance for Live2 Languages -- 5 Live3 Languages -- References -- Temporal Causality in Reactive Systems -- 1 Introduction -- 2 Preliminaries -- 3 Motivating Example -- 4 Property Causality -- 4.1 Interventions -- 4.2 Contingencies -- 4.3 Actual Causality for Trace Properties -- 5 Checking -Regular Causality -- 5.1 Interventions -- 5.2 Contingencies -- 5.3 Minimality -- 5.4 Deciding -Regular Causality -- 6 Related Work -- 7 Conclusion -- References -- PDAAAL: A Library for Reachability Analysis of Weighted Pushdown Systems -- 1 Introduction -- 2 Weighted Pushdown Systems and Reachability -- 3 Implemented Algorithms and PDAAAL Architecture -- 4 Comparison with State-of-the-Art -- 5 Applications -- 6 Conclusion -- References -- Active Learning -- Learning Deterministic One-Clock Timed Automata via Mutation Testing -- 1 Introduction -- 2 Preliminaries -- 2.1 Deterministic One-Clock Timed Automata -- 2.2 Active Learning Algorithm for DOTAs -- 2.3 Model-Based Mutation Testing. 3 Mutation-Based Testing for DOTAs -- 3.1 The Process Overview -- 3.2 Heuristic Test-Case Generation -- 3.3 Mutation and Score-Based Test-Case Selection -- 4 Learning-Friendly Mutation Operators for DOTAs -- 4.1 Timed Mutation Operator -- 4.2 Split-Location Mutation Operator -- 5 Implementation and Experiments -- 5.1 Case Studies -- 5.2 Evaluation of Improvements -- 6 Conclusion -- References -- Active Learning of One-Clock Timed Automata Using Constraint Solving -- 1 Introduction -- 2 Preliminaries -- 3 Learning Algorithm -- 3.1 Alignment and Comparison of Timed Words -- 3.2 Timed Observation Table -- 3.3 Encoding of Readiness Constraints -- 3.4 Hypothesis Construction -- 3.5 Main Algorithm and Correctness -- 4 Extension to Deterministic Timed Mealy Machines -- 5 Implementation and Experiments -- 5.1 Experiments on DOTAs -- 5.2 Experiments on TMMs -- 6 Conclusion -- References -- Learning and Characterizing Fully-Ordered Lattice Automata -- 1 Introduction -- 2 Preliminaries -- 3 A Myhill-Nerode Characterization for FOLAs -- 3.1 No Unique Minimal FOLA -- 3.2 Difficulties in Defining f -- 3.3 Defining the Equivalence Relation -- 3.4 The Correspondence Between f and a Minimal FOLA -- 4 The Learning Algorithm -- 5 Empirical Results -- 6 Conclusions -- References -- Probabilistic and Stochastic Systems -- Optimistic and Topological Value Iteration for Simple Stochastic Games -- 1 Introduction -- 2 Preliminaries -- 2.1 Simple Stochastic Games -- 2.2 Value Iteration and Bounded Value Iteration -- 3 Optimistic Value Iteration -- 4 Precise Topological Value Iteration -- 5 Random Generation of Simple Stochastic Games -- 6 Experiments -- 6.1 Experimental Setup -- 6.2 Overview -- 6.3 Detailed Analysis of Precise Algorithms -- 6.4 Detailed Analysis of Approximate (-Precise) Algorithms -- 7 Conclusion -- References -- Alternating Good-for-MDPs Automata. 1 Introduction. |
| Record Nr. | UNINA-9910620200703321 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated technology for verification and analysis : 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-21, 2021, proceedings / / Zhe Hou, Vijay Ganesh (editors)
| Automated technology for verification and analysis : 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-21, 2021, proceedings / / Zhe Hou, Vijay Ganesh (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (384 pages) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Automatic theorem proving
Computer logic |
| ISBN | 3-030-88885-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910502588603321 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated technology for verification and analysis : 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-21, 2021, proceedings / / Zhe Hou, Vijay Ganesh (editors)
| Automated technology for verification and analysis : 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-21, 2021, proceedings / / Zhe Hou, Vijay Ganesh (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (384 pages) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Automatic theorem proving
Computer logic |
| ISBN | 3-030-88885-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996464402003316 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated technology for verification and analysis : 6th international symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008 : proceedings / / Sungdeok Cha [and three others] editors
| Automated technology for verification and analysis : 6th international symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008 : proceedings / / Sungdeok Cha [and three others] editors |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer-Verlag, , [2008] |
| Descrizione fisica | 1 online resource (XIV, 430 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-540-88387-8 |
| Classificazione | 54.52 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Tests, Proofs and Refinements -- Formal Verification and Biology -- Trust and Automation in Verification Tools -- Model Checking -- CTL Model-Checking with Graded Quantifiers -- Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms -- Computation Tree Regular Logic for Genetic Regulatory Networks -- Compositional Verification for Component-Based Systems and Application -- A Direct Algorithm for Multi-valued Bounded Model Checking -- Software Verification -- Model Checking Recursive Programs with Exact Predicate Abstraction -- Loop Summarization Using Abstract Transformers -- Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions -- Decision Procedures -- Automating Algebraic Specifications of Non-freely Generated Data Types -- Interpolants for Linear Arithmetic in SMT -- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems -- SMELS: Satisfiability Modulo Equality with Lazy Superposition -- Linear-Time Analysis -- Controllable Test Cases for the Distributed Test Architecture -- Tool Demonstration Papers -- Goanna: Syntactic Software Model Checking -- A Dynamic Assertion-Based Verification Platform for Validation of UML Designs -- CheckSpec: A Tool for Consistency and Coverage Analysis of Assertion Specifications -- DiVinE Multi-Core – A Parallel LTL Model-Checker -- Alaska -- NetQi: A Model Checker for Anticipation Game -- Component-Based Design and Analysis of Embedded Systems with UPPAAL PORT -- Timed and Stochastic Systems -- Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions -- Decidable Compositions of O-Minimal Automata -- On the Applicability of Stochastic Petri Nets for Analysis of Multiserver Retrial Systems with Different Vacation Policies -- Model Based Importance Analysis for Minimal Cut Sets -- Theory -- Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic -- Tree Pattern Rewriting Systems -- Deciding Bisimilarity of Full BPA Processes Locally -- Optimal Strategy Synthesis in Request-Response Games -- Short Papers -- Authentication Revisited: Flaw or Not, the Recursive Authentication Protocol -- Impartial Anticipation in Runtime-Verification -- Run-Time Monitoring of Electronic Contracts -- Practical Efficient Modular Linear-Time Model-Checking -- Passive Testing of Timed Systems. |
| Record Nr. | UNISA-996465921503316 |
| Berlin, Heidelberg : , : Springer-Verlag, , [2008] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated technology for verification and analysis : 6th international symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008 : proceedings / / Sungdeok Cha [and three others] editors
| Automated technology for verification and analysis : 6th international symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008 : proceedings / / Sungdeok Cha [and three others] editors |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer-Verlag, , [2008] |
| Descrizione fisica | 1 online resource (XIV, 430 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-540-88387-8 |
| Classificazione | 54.52 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Tests, Proofs and Refinements -- Formal Verification and Biology -- Trust and Automation in Verification Tools -- Model Checking -- CTL Model-Checking with Graded Quantifiers -- Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms -- Computation Tree Regular Logic for Genetic Regulatory Networks -- Compositional Verification for Component-Based Systems and Application -- A Direct Algorithm for Multi-valued Bounded Model Checking -- Software Verification -- Model Checking Recursive Programs with Exact Predicate Abstraction -- Loop Summarization Using Abstract Transformers -- Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions -- Decision Procedures -- Automating Algebraic Specifications of Non-freely Generated Data Types -- Interpolants for Linear Arithmetic in SMT -- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems -- SMELS: Satisfiability Modulo Equality with Lazy Superposition -- Linear-Time Analysis -- Controllable Test Cases for the Distributed Test Architecture -- Tool Demonstration Papers -- Goanna: Syntactic Software Model Checking -- A Dynamic Assertion-Based Verification Platform for Validation of UML Designs -- CheckSpec: A Tool for Consistency and Coverage Analysis of Assertion Specifications -- DiVinE Multi-Core – A Parallel LTL Model-Checker -- Alaska -- NetQi: A Model Checker for Anticipation Game -- Component-Based Design and Analysis of Embedded Systems with UPPAAL PORT -- Timed and Stochastic Systems -- Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions -- Decidable Compositions of O-Minimal Automata -- On the Applicability of Stochastic Petri Nets for Analysis of Multiserver Retrial Systems with Different Vacation Policies -- Model Based Importance Analysis for Minimal Cut Sets -- Theory -- Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic -- Tree Pattern Rewriting Systems -- Deciding Bisimilarity of Full BPA Processes Locally -- Optimal Strategy Synthesis in Request-Response Games -- Short Papers -- Authentication Revisited: Flaw or Not, the Recursive Authentication Protocol -- Impartial Anticipation in Runtime-Verification -- Run-Time Monitoring of Electronic Contracts -- Practical Efficient Modular Linear-Time Model-Checking -- Passive Testing of Timed Systems. |
| Record Nr. | UNINA-9910768461503321 |
| Berlin, Heidelberg : , : Springer-Verlag, , [2008] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated theorem proving : after 25 years / / W.W. Bledsoe and D.W. Loveland, editors
| Automated theorem proving : after 25 years / / W.W. Bledsoe and D.W. Loveland, editors |
| Pubbl/distr/stampa | Providence, Rhode Island : , : American Mathematical Society, , [1984] |
| Descrizione fisica | 1 online resource (371 p.) |
| Disciplina | 511.3 |
| Collana | Contemporary mathematics |
| Soggetto topico | Automatic theorem proving |
| Soggetto genere / forma | Electronic books. |
| ISBN |
0-8218-7614-7
0-8218-5383-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
""Table of Contents""; ""Preface""; ""Acknowledgments""; ""Automated Theorem Proving: a Quarter Century Review""; ""Citation to Hao Wang""; ""Computer Theorem Proving and Artificial Intelligence""; ""Citation to Lawrence Wos and Steven Winker""; ""Open Questions Solved with the Assistance of AURA""; ""Some Automatic Proofs in Analysis""; ""Proof-Checking, Theorem-Proving, and Program Verification""; ""A Mechanical Proof of the Turing Completeness of Pure LISP""; ""Automating Higher-order Logic""; ""Abelian Group Unification Algorithms for Elementary Terms""
""Combining Satisfiability Procedures by Equality Sharing""""On the Decision Problem and the Mechanization of Theorem-Proving in Elementary Geometry""; ""Some Recent Advances in Mechanical Theorem-proving of Geometries""; ""Proving Elementary Geometry Theorems Using Wu's Algorithm""; ""Automated Theory Formation in Mathematics""; ""Student Use of an Interactive Theorem Prover"" |
| Record Nr. | UNINA-9910480620003321 |
| Providence, Rhode Island : , : American Mathematical Society, , [1984] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated theorem proving : after 25 years / / W.W. Bledsoe and D.W. Loveland, editors
| Automated theorem proving : after 25 years / / W.W. Bledsoe and D.W. Loveland, editors |
| Pubbl/distr/stampa | Providence, Rhode Island : , : American Mathematical Society, , [1984] |
| Descrizione fisica | 1 online resource (371 p.) |
| Disciplina | 511.3 |
| Collana | Contemporary mathematics |
| Soggetto topico | Automatic theorem proving |
| ISBN |
0-8218-7614-7
0-8218-5383-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Table of Contents -- Preface -- Acknowledgments -- Automated Theorem Proving: a Quarter Century Review -- Citation to Hao Wang -- Computer Theorem Proving and Artificial Intelligence -- Citation to Lawrence Wos and Steven Winker -- Open Questions Solved with the Assistance of AURA -- Some Automatic Proofs in Analysis -- Proof-Checking, Theorem-Proving, and Program Verification -- A Mechanical Proof of the Turing Completeness of Pure LISP -- Automating Higher-order Logic -- Abelian Group Unification Algorithms for Elementary Terms -- Combining Satisfiability Procedures by Equality Sharing -- On the Decision Problem and the Mechanization of Theorem-Proving in Elementary Geometry -- Some Recent Advances in Mechanical Theorem-proving of Geometries -- Proving Elementary Geometry Theorems Using Wu's Algorithm -- Automated Theory Formation in Mathematics -- Student Use of an Interactive Theorem Prover. |
| Record Nr. | UNINA-9910788782203321 |
| Providence, Rhode Island : , : American Mathematical Society, , [1984] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated theorem proving : after 25 years / / W.W. Bledsoe and D.W. Loveland, editors
| Automated theorem proving : after 25 years / / W.W. Bledsoe and D.W. Loveland, editors |
| Pubbl/distr/stampa | Providence, Rhode Island : , : American Mathematical Society, , [1984] |
| Descrizione fisica | 1 online resource (371 p.) |
| Disciplina | 511.3 |
| Collana | Contemporary mathematics |
| Soggetto topico | Automatic theorem proving |
| ISBN |
0-8218-7614-7
0-8218-5383-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Table of Contents -- Preface -- Acknowledgments -- Automated Theorem Proving: a Quarter Century Review -- Citation to Hao Wang -- Computer Theorem Proving and Artificial Intelligence -- Citation to Lawrence Wos and Steven Winker -- Open Questions Solved with the Assistance of AURA -- Some Automatic Proofs in Analysis -- Proof-Checking, Theorem-Proving, and Program Verification -- A Mechanical Proof of the Turing Completeness of Pure LISP -- Automating Higher-order Logic -- Abelian Group Unification Algorithms for Elementary Terms -- Combining Satisfiability Procedures by Equality Sharing -- On the Decision Problem and the Mechanization of Theorem-Proving in Elementary Geometry -- Some Recent Advances in Mechanical Theorem-proving of Geometries -- Proving Elementary Geometry Theorems Using Wu's Algorithm -- Automated Theory Formation in Mathematics -- Student Use of an Interactive Theorem Prover. |
| Record Nr. | UNINA-9910828935003321 |
| Providence, Rhode Island : , : American Mathematical Society, , [1984] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
