Dynamic Logic. New Trends and Applications: Second International Workshop, DaLí 2019, Porto, Portugal, October 7–11, 2019, Proceedings (Lecture Notes in Computer Science Book 12005)

This book constitutes the proceedings of the Second International Workshop on Dynamic Logic, DALI 2019, held in Porto, Portugal in October 2019. The workshop was held in Porto, Portugal, on October 9, 2019, as part of the Formal Methods Week which hosted the 3rd World Congress on Formal Methods. The 12 full papers presented together with 2 short papers were carefully reviewed and selected from 26 submissions. The workshop is based on the project DaLí – Dynamic logics for cyber-physical systems: towards contract based design. Preface Organization Contents Regular Papers Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq 1 Introduction 2 Basic Definitions 3 Bisimulations 4 Formalization in Coq 4.1 The Coq Proof Assistant in a Nutshell 4.2 Formalizing Relation-Changing Logics in Coq 5 Final Remarks References Behavioural and Abstractor Specifications for a Dynamic Logic with Binders and Silent Transitions 1 Introduction 2 A Dynamic Logic with Binders and Silent Transitions 3 Abstractor and Behavioural Specifications over D"3223379 3.1 Motivation and Example 3.2 Abstractor Specifications over D"3223379 3.3 Behavioural Specifications over D"3223379 4 Behaviour-Abstractor Framework for D"3223379 -logic 4.1 Behaviour-Abstractor Framework 4.2 Instantiation of the Behaviour-Abstractor Framework with D"3223379 5 Concluding Remarks References The Logic of AGM Learning from Partial Observations 1 Introduction 2 Syntax and Semantics 2.1 Expressive Power of L and Its Fragments 3 Expressing Belief and Notions of Learnability 4 A Complete Proof System 4.1 Axiomatization 4.2 Soundness and Completeness 5 Conclusions and Open Questions References A Dynamic Epistemic Logic Analysis of the Equality Negation Task 1 Introduction 2 Preliminaries 2.1 Topological Models for Dynamic Epistemic Logic (DEL) 2.2 The Layered Message-Passing Action Model 2.3 Outline of Impossibility Proofs 3 Equality Negation Task for Two Processes 3.1 DEL Analysis of the Task 3.2 Bisimulation and Limits of the DEL Framework 3.3 Extended DEL 4 Conclusion References A Logical Analysis of the Interplay Between Social Influence and Friendship Selection 1 Introduction 2 Social Network Models 3 Social Networks Dynamics 3.1 Social Environment Influencing Agents 3.2 Agents Creating Their Social Environment 3.3 Intertwining Dynamics 4 Variations 5 Conclusions References A Four-Valued Hybrid Logic with Non-dual Modal Operators 1 Introduction 2 Double-Belnapian Hybrid Logic 2.1 Syntax for Double-Belnapian Hybrid Logic 2.2 Semantics for Double-Belnapian Hybrid Logic 2.3 A Tableau System for Double-Belnapian Hybrid Logic 2.4 Representation of Models via Diagrams 3 Conclusion References Persuasive Argumentation and Epistemic Attitudes 1 Introduction 2 Persuasive Communication 2.1 Preliminaries 2.2 Communication and Persuasion 3 A Dynamic Epistemic Logic for Argumentation 3.1 Syntax and Semantics of L 3.2 A Dynamic Extension of L 3.3 Completeness 4 Epistemic-Based Persuasive Arguments 5 Closing Words and Future Work References The Trace Modality 1 Introduction 2 Programs, Logic, Traces and Abstractions 3 The Trace Modality 3.1 Functional Verification 3.2 Information Flow Analysis 3.3 Software Model Checking 3.4 Program Synthesis 3.5 Correct Compilation 3.6 Program Evolution and Bug Fixing 4 Reasoning About the Trace Modality 5 Related Work 6 Conclusion and Outlook References Iterative Division in the Distributive Full Non-associative Lambek Calculus 1 Introduction 2 Relational Models and Iteration 3 Completeness and Decidability 4 Conclusion References Resource Separation in Dynamic Logic of Propositional Assignments 1 Introduction 2 Models and Their Splitting and Merging 3 Language 4 Semantics 5 Axiomatisation via Reduction Axioms 5.1 Copies of Atomic Propositions 5.2 Useful Programs 5.3 Useful Formulas 5.4 Reduction Axioms for Program Operators 5.5 Reduction Axioms for Boolean Operators 5.6 Reduction Axioms for Assignments 5.7 Soundness, Completeness, and Decidability 6 Complexity via Translation into DL-PA 7 Conclusion References Stit Semantics for Epistemic Notions Based on Information Disclosure in Interactive Settings 1 Introduction 2 An Example Involving Four Kinds of Game Knowledge 3 Ex Ante, Ex interim, Ex Post, and Know-How 4 Axiomatization 5 Conclusion References Bringing Belief Base Change into Dynamic Epistemic Logic 1 Introduction 2 Dynamic and Iterated Belief Change 3 Dynamic Preference Logic 3.1 Preferences and Priorities 4 Iterated Belief Change and Dynamic Preference Logic 4.1 Characterising Relevant Graph Transformations 4.2 Overcoming P-Graphs Expressibility Gaps 5 Final Considerations References Short Papers A Dynamic Logic for QASM Programs 1 Introduction 2 Quantum Computing 2.1 States 2.2 Transitions (programs) 2.3 Acceptance States 3 A Dynamic Logic for QASM 3.1 Syntax 3.2 Semantics 3.3 The State Space 3.4 Propositions 3.5 Program Semantics 4 An Example: A Quantum Coin Tossing Program 5 Conclusions References On the Construction of Multi-valued Concurrent Dynamic Logics 1 Introduction 2 Preliminaries 2.1 Semantics for Concurrency 2.2 Concurrent Propositional Dynamic Logic 2.3 Parametric Construction of Multi-valued Dynamic Logics 3 Multi-valued Concurrent Dynamic Logic 3.1 Fuzzy Binary Multirelations 3.2 Parametric Construction of Multi-valued Concurrent Dynamic Logics 4 Conclusion References Author Index This book constitutes the proceedings of the Second International Workshop on Dynamic Logic, DALI 2019, held in Porto, Portugal in October 2019. The workshop was held in Porto, Portugal, on October 9, 2019, as part of the Formal Methods Week which hosted the 3rd World Congress on Formal Methods. The 12 full papers presented together with 2 short papers were carefully reviewed and selected from 26 submissions. The workshop is based on the project DaLí - Dynamic logics for cyber-physical systems: towards contract based design. .