Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2018 | Book

Undecidability of Relation-Changing Modal Logics Read chapter Read first chapter

Dynamic Logic. New Trends and Applications

First International Workshop, DALI 2017, Brasilia, Brazil, September 23-24, 2017, Proceedings

Editors: Alexandre Madeira, Mário Benevides

Publisher: Springer International Publishing

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

This book constitutes the proceedings of the First International Workshop on Dynamic Logic, DALI 2017, held in Brasilia, Brazil, in September 2017.
Both its theoretical relevance and practical potential make Dynamic Logic a topic of interest in a number of scientific venues, from wide-scope software engineering conferences to modal logic specific events. The workshop is promoted by an R&D project on dynamic logics for cyber-physical systems. The 12 full papers presented in this volume were carefully reviewed and selected from 25 submissions. The workshop is based on the project DaLí – Dynamic logics for cyber-physical systems: towards contract based design.

Table of Contents

Frontmatter
Undecidability of Relation-Changing Modal Logics
Abstract
Relation-changing modal logics are extensions of the basic modal logic that allow to change the accessibility relation of a model during the evaluation of a formula. In particular, they are equipped with dynamic modalities that are able to delete, add and swap edges in the model, both locally and globally. We investigate the satisfiability problem of these logics. We define satisfiability-preserving translations from an undecidable memory logic to relation-changing modal logics. This way we show that their satisfiability problems are undecidable.
Carlos Areces, Raul Fervari, Guillaume Hoffmann, Mauricio Martel
Axiomatization and Computability of a Variant of Iteration-Free PDL with Fork
Abstract
We devote this paper to the axiomatization and the computability of \(PDL^{\varDelta }_{0}\)—a variant of iteration-free PDL with fork.
Philippe Balbiani, Joseph Boudou
A Dynamic Logic for Learning Theory
Abstract
Building on previous work [4, 5] that bridged Formal Learning Theory and Dynamic Epistemic Logic in a topological setting, we introduce a Dynamic Logic for Learning Theory (DLLT), extending Subset Space Logics [9, 17] with dynamic observation modalities \([o]\varphi \), as well as with a learning operator https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-73579-5_3/461709_1_En_3_IEq2_HTML.gif , which encodes the learner’s conjecture after observing a finite sequence of data https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-73579-5_3/461709_1_En_3_IEq3_HTML.gif . We completely axiomatise DLLT, study its expressivity and use it to characterise various notions of knowledge, belief, and learning.
Alexandru Baltag, Nina Gierasimczuk, Aybüke Özgün, Ana Lucia Vargas Sandoval, Sonja Smets
Layered Logics, Coalgebraically
Abstract
This note revisits layered logics from a coalgebraic point of view, and proposes a naturality condition to express the typical hierarchical requirement under which all abstract transitions should be traceable in more specialised layers.
Luís Soares Barbosa
A Dynamic Informational-Epistemic Logic
Abstract
Epistemic logic is usually employed to model two aspects of a situation: the ontic and the epistemic aspects. Truth, however, is not always attainable, and in many cases we are forced to reason only with whatever information is available to us. In this paper, we will explore a four-valued epistemic logic designed to deal with situations of this sort. The technical results include a set of reduction axioms for public announcements, correspondence proofs, and a complete tableau system.
Yuri David Santos
Dynamic Epistemic Logics of Introspection
Abstract
This work studies positive and negative introspection not as properties, but rather as actions that change the agent’s knowledge. The actions are introduced as model update operations, with matching modalities expressing their effects. Sound and complete axiom systems are provided, and some properties are explored.
Raul Fervari, Fernando R. Velázquez-Quesada
Logics for Actor Networks: A Case Study in Constrained Hybridization
A Case Study in Constrained Hybridization
Abstract
Actor Networks are a modeling framework for cyber-physical system protocols based on Latour’s actor-network theory that addresses the way we now create and exploit the power of computational networks. We advance a logic for modeling and reasoning about such actor networks, which is obtained through a two-stage constrained hybridization process. The first stage results in a logic that captures the structure of actor networks and the way knowledge flows across them; the second addresses the dynamic aspects of actor networks, that is the way they can evolve as a result of the interactions that occur within them. For each of these stages, we develop a sound and complete proof system.
José Fiadeiro, Ionuţ Ţuţu, Antónia Lopes, Dusko Pavlovic
Parity Games and Automata for Game Logic
Abstract
Parikh’s game logic is a PDL-like fixpoint logic interpreted on monotone neighbourhood frames that represent the strategic power of players in determined two-player games. Game logic translates into a fragment of the monotone \(\mu \)-calculus, which in turn is expressively equivalent to monotone modal automata. Parity games and automata are important tools for dealing with the combinatorial complexity of nested fixpoints in modal fixpoint logics, such as the modal \(\mu \)-calculus. In this paper, we (1) discuss the semantics a of game logic over neighbourhood structures in terms of parity games, and (2) use these games to obtain an automata-theoretic characterisation of the fragment of the monotone \(\mu \)-calculus that corresponds to game logic. Our proof makes extensive use of structures that we call syntax graphs that combine the ease-of-use of syntax trees of formulas with the flexibility and succinctness of automata. They are essentially a graph-based view of the alternating tree automata that were introduced by Wilke in the study of modal \(\mu \)-calculus.
Helle Hvid Hansen, Clemens Kupke, Johannes Marti, Yde Venema
Model Checking Against Arbitrary Public Announcement Logic: A First-Order-Logic Prover Approach for the Existential Fragment
Abstract
In this paper, we investigate the model checking problem of symbolic models against epistemic logic with arbitrary public announcements and group announcements. We reduce this problem to the satisfiability of Monadic Monadic Second Order Logic (MMSO), the fragment of monadic-second order logic restricted to monadic predicates. In particular, for the case of epistemic formulas in which all arbitrary and group announcements are existential, the proposed reduction lands in monadic first-order logic. We take advantage of this situation to report on few experiments we made with first-order provers.
Tristan Charrier, Sophie Pinchinat, François Schwarzentruber
Dynamic Logic: A Personal Perspective
Abstract
We review a few of the developments of dynamic logic from the author’s perspective. As implied by the title the review is not intended as a survey of the field as a whole but rather as how the author’s outlook on imperative programs and their logics evolved during the four decades up to the start of this millennium.
Vaughan Pratt
The Creation and Change of Social Networks: A Logical Study Based on Group Size
Abstract
This paper is part of an on-going programme in which we provide a logical study of social network formations. In the proposed setting, agent a will consider agent b as part of her network if the number of features (properties) on which they differ is small enough, given the constraints on the size of agent a’s ‘social space’. We import this idea about a limit on one’s social space from the cognitive science literature. In this context we study the creation of new networks and use the tools of Dynamic Epistemic Logic to model the updates of the networks. By providing a set of reduction axioms we are able to provide sound and complete axiomatizations for the logics studied in this paper.
Sonja Smets, Fernando R. Velázquez-Quesada
Dynamic Preference Logic as a Logic of Belief Change
Abstract
AGM’s belief revision is one of the main paradigms in the study of belief change operations. Recently, several logics for belief and information change have been proposed in the literature, which were used to encode belief change operations in a rich and expressive framework. While the connection of AGM-like operations and their encoding in dynamic doxastic logics have been studied before, by the exceptional work of Segerberg, most work on the area of Dynamic Epistemic Logics (DEL) have not attempted to characterize belief change operators by means of their logical properties. This work investigates how Dynamic Preference Logic, a logic in the DEL family, can be used to characterise properties of dynamic belief change operators, focusing on well-known postulates of iterated belief change.
Marlo Souza, Álvaro Moreira, Renata Vieira
Backmatter
Metadata
Title
Dynamic Logic. New Trends and Applications
Editors
Alexandre Madeira
Mário Benevides
Copyright Year
2018
Electronic ISBN
978-3-319-73579-5
Print ISBN
978-3-319-73578-8
DOI
https://doi.org/10.1007/978-3-319-73579-5

Premium Partner

    Image Credits