Dynamic Logic New Trends and

Full download test bank at ebook textbookfull.
com
Dynamic Logic New Trends and

Applications First International
Workshop DALI 2017 Brasilia Brazil
September 23 24 2017 Proceedings
CLICK LINK TO DOWLOAD
https://textbookfull.com/product/dynamic-
logic-new-trends-and-applications-first-
international-workshop-dali-2017-brasilia-
brazil-september-23-24-2017-proceedings-1st-
edition-alexandre-madeira/
textbookfull
More products digital (pdf, epub, mobi) instant
download maybe you interests ...
Logic, Language, Information, and Computation: 24th

International Workshop, WoLLIC 2017, London, UK, July
18-21, 2017, Proceedings 1st Edition Juliette Kennedy
https://textbookfull.com/product/logic-language-information-and-
computation-24th-international-workshop-wollic-2017-london-uk-
july-18-21-2017-proceedings-1st-edition-juliette-kennedy/
Mobility Analytics for Spatio Temporal and Social Data

First International Workshop MATES 2017 Munich Germany
September 1 2017 Revised Selected Papers 1st Edition
Christos Doulkeridis
https://textbookfull.com/product/mobility-analytics-for-spatio-
temporal-and-social-data-first-international-workshop-
mates-2017-munich-germany-september-1-2017-revised-selected-
papers-1st-edition-christos-doulkeridis/
Analytical and Computational Methods in Probability

Theory First International Conference ACMPT 2017 Moscow
Russia October 23 27 2017 Proceedings 1st Edition
Vladimir V. Rykov
https://textbookfull.com/product/analytical-and-computational-
methods-in-probability-theory-first-international-conference-
acmpt-2017-moscow-russia-october-23-27-2017-proceedings-1st-
edition-vladimir-v-rykov/
Provable Security: 11th International Conference,

ProvSec 2017, Xi’an, China, October 23-25, 2017,
Proceedings 1st Edition Tatsuaki Okamoto
https://textbookfull.com/product/provable-security-11th-
international-conference-provsec-2017-xian-china-
october-23-25-2017-proceedings-1st-edition-tatsuaki-okamoto/
Algorithms and Complexity 10th International Conference
CIAC 2017 Athens Greece May 24 26 2017 Proceedings 1st
Edition Dimitris Fotakis
https://textbookfull.com/product/algorithms-and-complexity-10th-
international-conference-ciac-2017-athens-greece-
may-24-26-2017-proceedings-1st-edition-dimitris-fotakis/
Interactive Storytelling 10th International Conference

on Interactive Digital Storytelling ICIDS 2017 Funchal
Madeira Portugal November 14 17 2017 Proceedings 1st
Edition Nuno Nunes
https://textbookfull.com/product/interactive-storytelling-10th-
international-conference-on-interactive-digital-storytelling-
icids-2017-funchal-madeira-portugal-
november-14-17-2017-proceedings-1st-edition-nuno-nunes/
ICIBSoS 2017 : Proceedings of the 6th International

Congress on Interdisciplinary Behavior and Social
Sciences (ICIBSoS 2017), July 22-23, 2017, ANVAYA Beach
Resort, Bali, Indonesia First Edition Lumban Gaol
https://textbookfull.com/product/icibsos-2017-proceedings-of-
the-6th-international-congress-on-interdisciplinary-behavior-and-
social-sciences-icibsos-2017-july-22-23-2017-anvaya-beach-resort-
bali-indonesia-first-edition-lumb/
Exploring Services Science 8th International Conference

IESS 2017 Rome Italy May 24 26 2017 Proceedings 1st
Edition Stefano Za
https://textbookfull.com/product/exploring-services-science-8th-
international-conference-iess-2017-rome-italy-
may-24-26-2017-proceedings-1st-edition-stefano-za/
Cyberspace Safety and Security 9th International

Symposium CSS 2017 Xi an China October 23 25 2017
Proceedings 1st Edition Sheng Wen
https://textbookfull.com/product/cyberspace-safety-and-
security-9th-international-symposium-css-2017-xi-an-china-
october-23-25-2017-proceedings-1st-edition-sheng-wen/
Alexandre Madeira
Mário Benevides (Eds.)
LNCS 10669
Dynamic Logic
New Trends and Applications
First International Workshop, DALI 2017
Brasilia, Brazil, September 23–24, 2017
Proceedings
123
Lecture Notes in Computer Science 10669
Commenced Publication in 1973
Founding and Former Series Editors:
Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen
Editorial Board
David Hutchison
Lancaster University, Lancaster, UK
Takeo Kanade
Carnegie Mellon University, Pittsburgh, PA, USA
Josef Kittler
University of Surrey, Guildford, UK
Jon M. Kleinberg
Cornell University, Ithaca, NY, USA
Friedemann Mattern
ETH Zurich, Zurich, Switzerland
John C. Mitchell
Stanford University, Stanford, CA, USA
Moni Naor
Weizmann Institute of Science, Rehovot, Israel
C. Pandu Rangan
Indian Institute of Technology, Madras, India
Bernhard Steffen
TU Dortmund University, Dortmund, Germany
Demetri Terzopoulos
University of California, Los Angeles, CA, USA
Doug Tygar
University of California, Berkeley, CA, USA
Gerhard Weikum
Max Planck Institute for Informatics, Saarbrücken, Germany
More information about this series at http://www.springer.com/series/7407
Alexandre Madeira Mário Benevides (Eds.)
•
Dynamic Logic
New Trends and Applications
First International Workshop, DALI 2017
Brasilia, Brazil, September 23–24, 2017
Proceedings
123
Editors
Alexandre Madeira Mário Benevides
INESC TEC UFRJ
University of Minho Rio de Janeiro
Braga Brazil
Portugal
and
CIDMA
University Aveiro
Aveiro
Portugal
ISSN 0302-9743 ISSN 1611-3349 (electronic)

Lecture Notes in Computer Science
ISBN 978-3-319-73578-8 ISBN 978-3-319-73579-5 (eBook)
https://doi.org/10.1007/978-3-319-73579-5
Library of Congress Control Number: 2017962907
LNCS Sublibrary: SL1 – Theoretical Computer Science and General Issues
© Springer International Publishing AG 2018

This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of the
material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation,
broadcasting, reproduction on microfilms or in any other physical way, and transmission or information
storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now
known or hereafter developed.
The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication
does not imply, even in the absence of a specific statement, that such names are exempt from the relevant
protective laws and regulations and therefore free for general use.
The publisher, the authors and the editors are safe to assume that the advice and information in this book are
believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors
give a warranty, express or implied, with respect to the material contained herein or for any errors or
omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in
published maps and institutional affiliations.
Printed on acid-free paper
This Springer imprint is published by Springer Nature

The registered company is Springer International Publishing AG
The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland
Preface
Building on the pioneer intuitions of Floyd–Hoare logic, dynamic logic was introduced
in the 1970s by Vaughan Pratt as a suitable logic to reason about, and verify, classic
imperative programs. Since then, the original intuitions grew to an entire family of
logics, which became increasingly popular for assertional reasoning about a wide range
of computational systems. Simultaneously, their object (i.e., the very notion of a
program) evolved in unexpected ways. This leads to dynamic logics tailored to specific
programming paradigms and extended to new computing domains, including proba-
bilistic, continuous, and quantum computation. 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. However, as far as we know, to date, no specific event was exclusively dedi-
cated to it. This workshop emerged from this discussion, during the kick-off meeting
of the project DaLí - Dynamic Logics for Cyber-Physical Systems, whose editors are
participating as consultant and IR, respectively.
This volume contains the proceedings of the event that was held in the beautiful city
of Brasilia during September 23–24, 2017, co-located with Tableaux, ITP, and FroCoS
2017.
We received 24 submissions, of which, after a careful revision process, with at least
three revisions per work, 12 papers were accepted as regular papers and are published
in this volume. Beyond these contributions, the workshop also included the following
short papers:
– Fabricio Chalub, Alexandre Rademaker, Edward Hermann Haeusler and Christiano
Braga: “Fixing the Proof of completeness of ALC Sequent Calculus”
– Diana Costa and Édi Duarte: “Checkers Game in Deontic Logic”
– Daniel Figueiredo and Manuel A. Martins: “Bisimulations for Reactive Frames”
– Konstantinos Gkikas and Alexandru Baltag: “Stable Beliefs and Conditional
Probability Spaces”
– Leandro Gomes: “Contract-Based Design for Software Verification”
– Luiz Carlos Pereira: “Constructive Fragments of Classical Modal Logic and the
Ecumenical Perspective”
– Carlos Tavares: “Toward a Quantum-Probabilistic Dynamic Logic”
From this list, four papers were originally submitted as short contribution and the
other three were regular submissions invited to be converted into a short format. An
informal volume with the extended abstracts (3–5 pages) of these contributions was
provided in the conference.
We also had the invited talks of Alexandru Baltag, “Logic Goes Viral: Dynamic
Modalities for Social Networks,” and of Edward Hermann Haeusler, “Propositional
Dynamic Logic with Petri Net Programs: A Discussion and a Logical System”; the
latter is a joint work with Bruno Lopes and Mario Benevides. Finally, we had the
VI Preface
pleasure of hosting a special talk entitled “Dynamic Logic, a Personal Perspective,” by

the Dynamic Logics pioneer Vaughan Pratt.
The organization sincerely acknowledges the authors that submitted their works to
our workshop, to the Program Committee for their careful and attentive revisions, to the
Invited Speakers for their very interesting talks and to the local organizers for their
valuable and very prompt support.
September 2017 Mario Benevides

Alexandre Madeira
Organization
Conference Chairs
Mario Benevides UFRJ, Brazil
Alexandre Madeira University of Minho, Portugal
Program Committee
Carlos Areces University of Cordoba, Argentina
Phillippe Balbiani University of Toulouse, France
Alexandru Baltag Uva, The Netherlands
Luís S. Barbosa University of Minho, Portugal
Johan van Benthem University of Stanford, USA and University of Tsinghua,
China
Patrick Blackburn University of Roskilde, Denmark
Fredrik Dahlqvist UCL, UK
Stéphane Demri CNRS, France
Hans van Ditmarsch LORIA, Nancy, France
Francicleber M. Ferreira UFC, Brazil
Valentin Goranko University of Stockholm, Sweden
Edward H. Hauesler PUC-Rio, Brazil
Rolf Hennicker LMU, Munich, Germany
Andreas Herzig Toulouse, France
Dexter Kozen Cornell, USA
Clemens Kupke University of Strathclyde, UK
Bruno Lopes Vieira UFF, Brazil
Paulo Mateus IST, Portugal
Manuel A. Martins University of Aveiro, Portugal
Carlos Olarte UF RN, Brazil
José N. Oliveira University of Minho, Portugal
André Platzer CMU, USA
Eugénio Rocha University of Aveiro, Portugal
Valéria de Paiva NC, USA
Regivan Santiago UFRN, Brazil
Luis Menasche UFRJ, Brazil
Schechter
Tinko Tinchev Sofia University, Bulgaria
Petrucio Viana UFF, Brazil
Sheila Veloso UFRJ, Brazil
Yde Venema ILLC, The Netherlands
Renata Wassermann USP, Brazil
VIII Organization
Additional Reviewers
Brandon Bohrer
Diana Costa
Daniel Figueiredo
Isaque Lima
Vitor Machado
Johannes Marti
António Pereira
Elaine Pimentel
Sponsoring
This workshop was promoted by DaLí, a research project financed by the ERDF
European Regional Development Fund through the Operational Programme for
Competitiveness and Internationalization, COMPETE 2020 Program, and by National
Funds through the Portuguese funding agency, FCT, Fundação para a Ciência e a
Tecnologia, within reference POCI-01-0145-FEDER-016692.
FCT, Fundação para a Ciência e Tecnologia
CIDMA, Center for Research and Development in Mathematics and Applications
High Assurance Laboratory INESC TEC
Contents
Undecidability of Relation-Changing Modal Logics. . . . . . . . . . . . . . . . . . . 1

Carlos Areces, Raul Fervari, Guillaume Hoffmann,
and Mauricio Martel
Axiomatization and Computability of a Variant of Iteration-Free

PDL with Fork . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
Philippe Balbiani and Joseph Boudou
A Dynamic Logic for Learning Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

Alexandru Baltag, Nina Gierasimczuk, Aybüke Özgün,
Ana Lucia Vargas Sandoval, and Sonja Smets
Layered Logics, Coalgebraically . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

Luís Soares Barbosa
A Dynamic Informational-Epistemic Logic . . . . . . . . . . . . . . . . . . . . . . . . . 64

Yuri David Santos
Dynamic Epistemic Logics of Introspection . . . . . . . . . . . . . . . . . . . . . . . . 82

Raul Fervari and Fernando R. Velázquez-Quesada
Logics for Actor Networks: A Case Study in Constrained Hybridization . . . . 98

José Fiadeiro, Ionuţ Ţuţu, Antónia Lopes, and Dusko Pavlovic
Parity Games and Automata for Game Logic . . . . . . . . . . . . . . . . . . . . . . . 115

Helle Hvid Hansen, Clemens Kupke, Johannes Marti, and Yde Venema
Model Checking Against Arbitrary Public Announcement Logic:

A First-Order-Logic Prover Approach for the Existential Fragment . . . . . . . . 133
Tristan Charrier, Sophie Pinchinat, and François Schwarzentruber
Dynamic Logic: A Personal Perspective . . . . . . . . . . . . . . . . . . . . . . . . . . . 153

Vaughan Pratt
The Creation and Change of Social Networks: A Logical Study

Based on Group Size. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171
Sonja Smets and Fernando R. Velázquez-Quesada
Dynamic Preference Logic as a Logic of Belief Change. . . . . . . . . . . . . . . . 185

Marlo Souza, Álvaro Moreira, and Renata Vieira
Author Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201

Undecidability of Relation-Changing
Modal Logics
Carlos Areces1,2 , Raul Fervari1,2(B) , Guillaume Hoffmann1,2 ,

and Mauricio Martel3
1
FaMAF, Universidad Nacional de Córdoba, Córdoba, Argentina
{areces,fervari,hoffmann}@famaf.unc.edu.ar
2
Consejo Nacional de Investigaciones Cientı́ficas y Técnicas (CONICET),
Buenos Aires, Argentina
3
Fachbereich Mathematik und Informatik,
Universität Bremen, Bremen, Germany
martel@informatik.uni-bremen.de
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.
Keywords: Modal logics · Dynamic logics · Satisfiability

Undecidability
1 Introduction
Modal logics [12,14] were originally conceived as logics of necessary and possible
truths. They are now viewed, more broadly, as logics that explore a wide range
of modalities, or modes of truth: epistemic (“it is known that”), doxastic (“it is
believed that”), deontic (“it ought to be the case that”), or temporal (“it has
been the case that”), among others. From a model theoretic perspective, the
field evolved into a discipline that deals with languages interpreted on various
kinds of relational structures or graphs. Nowadays, modal logics are actively used
in areas as diverse as software verification, artificial intelligence, semantics and
pragmatics of natural language, law, philosophy, etc.
From an abstract point of view, modal logics can be seen as formal languages
to navigate and explore properties of a given relational structure. But if we
want to describe and reason about dynamic aspects of a given situation, e.g.,
how the relations between a set of elements evolve through time or through
the application of certain operations, the use of modal logics (or actually, any
kind of logic with classical semantics) becomes less clear. We can always resort
c Springer International Publishing AG 2018
A. Madeira and M. Benevides (Eds.): DALI 2017, LNCS 10669, pp. 1–16, 2018.
https://doi.org/10.1007/978-3-319-73579-5_1
2 C. Areces et al.
to modeling the whole space of possible evolutions as a graph, but this soon
becomes unwieldy. It would be more elegant to use truly dynamic modal logics
with operators that can mimic the changes the structure will undergo.
There exist several dynamic modal operators that fit in this approach. A
clear example are the dynamic operators introduced in dynamic epistemic logics
(see, e.g. [22]). Less obvious examples are given by hybrid logics [8,13] equipped
with the down arrow operator ↓ which is used to ‘rebind’ names for states to the
current point of evaluation, and memory logics [19], a kind of restricted form
of hybrid logics that come equipped with a memory and operators to store and
retrieve states from it. Finally, a classical example which can arguably be taken
as the origin of the studies of logics in this approach is Sabotage Logic introduced
by van Benthem in [21], which provides an operator that deletes individual edges
in the model.
Generalizing this last logic, we study operators that do various kinds of
change to the accessibility relation of a model: deleting, adding, and swapping
edges, both locally (near the state of evaluation) and globally (anywhere). We
call these operators relation-changing. In [2], the operators are introduced, and
it is shown that the model checking problem is PSPACE-complete for the basic
modal logic enriched with any of these operators. In this article, we consider
the satisfiability problem of these logics. Previous results on this topic are the
undecidability of (multimodal) global sabotage logic, via encoding of the Post
Correspondence Problem [16] the undecidability of local swap logic with a sin-
gle relation, by reduction from memory logic [4]; and non-terminating tableau
methods for all six logics [3]. Here we present undecidability proofs for all six
logics using reductions from memory logic.
The undecidability results can be surprising, considering for instance that
dynamic epistemic logics are decidable [11,17,22]. However, other very expres-
sive dynamic operators are undecidable, such as the hybrid logic with the ↓
operator [8]. As we mentioned before, ↓ binds states of the model to some par-
ticular names. We will show in this article that relation-changing operators can
take advantage of adding, deleting or swapping around edges, to perform some
sort of binding in the model, turning them undecidable.
Contributions
– We sketch the undecidability proof for the memory logic ML( r , k ), by adapt-
ing the undecidability argument introduced in [18] for the description logic
ALCself.
– We introduce undecidability proofs for the satisfiability problem of six relation-
changing modal logics via satisfiability of memory logic. In this way, we com-
plete the picture of the computational aspects of the family of languages
defined in this framework.
– Our proofs improve previous ones for local swap [4] and global sabotage [16],
by exploiting undecidability of memory logics. This allows for shorter proofs
and avoid redundant encodings of the tiling problem.
The article is organized as follows. In Sect. 2 we introduce the syntax and
semantics of relation-changing modal logics. In Sect. 3 we introduce the memory
Undecidability of Relation-Changing Modal Logics 3
logic ML( r , k ) and a sketch of the proof of its undecidability. We dedicate

Sect. 4 to the translations from memory to global and local relation-changing
modal logics. Finally we draw our conclusions in Sect. 5.
2 Relation-Changing Modal Logics

In this section, we formally introduce relation-changing modal logics. For more
details and motivations, we direct the reader to [15].
Definition 1 (Syntax). Let PROP be a countable, infinite set of propositional

symbols. The set FORM of formulas over PROP is defined as:
FORM ::= p | ¬ϕ | ϕ ∧ ψ | ♦ϕ | ϕ,
where p ∈ PROP, ∈ {sb, br, sw, gsb, gbr, gsw} and ϕ, ψ ∈ FORM.
Other operators are defined as usual. In particular, ϕ is defined as ¬¬ϕ.
Let ML (the basic modal logic) be the logic without the {sb, br, sw, gsb,
gbr, gsw} operators, and ML() the extension of ML allowing also , for
∈ {sb, br, sw, gsb, gbr, gsw}.
Semantically, formulas are evaluated in standard relational models, and the

meaning of the operators of the basic modal logic remains unchanged (see [12]
for details). When we evaluate formulas containing relation-changing operators,
we will need to keep track of the edges that have been modified. To that end, let
us define precisely the models that we will use.
Definition 2 (Models and model updates). A model M is a triple M =

W, R, V , where W is a non-empty set whose elements are called points or states,
R ⊆ W ×W is the accessibility relation, and V : PROP → P(W ) is a valuation.
We define the following notation:
(sabotaging) M− − −
S = W, RS , V , with RS = R\S, S ⊆ R.
(bridging) MS = W, RS , V , with RS = R ∪ S, S ⊆ (W ×W )\R.
+ + +
(swapping) M∗S = W, RS∗ , V , with RS∗ = (R\S −1 )∪S, S ⊆ R−1 .
Intuitively, M−
S is obtained from M by deleting the edges in S, and similarly
M+
S adds the edges in S to the accessibility relation, and M∗S adds the edges in
S as inverses of edges previously in the accessibility relation.
Let w be a state in M, the pair (M, w) is called a pointed model (we will
usually drop parentheses). In the rest of this article, we will use wv as a shorthand
for {(w, v)} or (w, v); context will always disambiguate the intended use.
4 C. Areces et al.
Definition 3 (Semantics). Given a pointed model M, w and a formula ϕ, we

say that M, w satisfies ϕ, and write M, w |= ϕ, when
M, w |= p iff w ∈ V (p)
M, w |= ¬ϕ iff M, w |= ϕ
M, w |= ϕ ∧ ψ iff M, w |= ϕ and M, w |= ψ
M, w |= ♦ϕ iff for some v ∈ W s.t. (w, v) ∈ R, M, v |= ϕ
M, w |= sbϕ iff for some v ∈ W s.t. (w, v) ∈ R, M− wv , v |= ϕ
M, w |= brϕ iff for some v ∈ W s.t. (w, v) ∈ R, M+ wv , v |= ϕ
M, w |= swϕ iff for some v ∈ W s.t. (w, v) ∈ R, M∗vw , v |= ϕ
M, w |= gsbϕ iff for some v, u ∈ W, s.t. (v, u) ∈ R, M−vu , w |= ϕ
M, w |= gbrϕ iff for some v, u ∈ W, s.t. (v, u) ∈ R, M+vu , w |= ϕ
M, w |= gswϕ iff for some v, u ∈ W, s.t. (v, u) ∈ R, M∗uv , w |= ϕ.
We say ϕ is satisfiable if for some pointed model M, w, we have M, w |= ϕ.

Notice that br and gbr always add new edges in the model, and fail in case
no new edge can be created. Other versions in which such edge is not necessarily
new could be considered, but in that case the operators would behave sometimes
as a ♦ or as a “do nothing”, respectively. However, we conjecture that similar
results could be proved for those and other versions of the operations.
Relation-changing operators can modify the accessibility relation and check
for such changes in the model, and therefore can be used to mark and check
for marked states, simulating some sort of binding. Adequately, marking and
checking states are the basic dynamic operations remember and known that can
be performed by memory logics, a formalism that we present in the next section.
3 Undecidability of Monomodal Memory Logic

Memory logics [1,19] are modal logics that can store the current state of evalua-
tion into a memory and check whether the current state belongs to this memory.
The memory is a subset of the domain of the model. We call ML( r , k ) the
memory logic that extends ML with the operators r and k , which stand for
“remember” and “known”, respectively.
Definition 4 (Syntax). Let PROP be a countable, infinite set of propositional
symbols. The set FORM of formulas over PROP is defined as:
FORM ::= p | k | ¬ϕ | ϕ ∧ ψ | ♦ϕ | r ϕ,
where p ∈ PROP and ϕ, ψ ∈ FORM. Other operators are defined as usual.

Definition 5 (Semantics). A model M = W, R, V, S is a relational model
equipped with a set S ⊆ W called the memory. Let w be a state in W . The
inductive definition of satisfiability for the cases specific to memory logic is:
W, R, V, S, w |= r ϕ iff W, R, V, S ∪ {w}, w |= ϕ

W, R, V, S, w |= k iff w ∈ S.
The remaining cases coincide with the semantics of ML, and do not involve the
memory.
An ML( r , k )-formula ϕ is satisfiable if there are a model M = W, R, V, ∅
and w ∈ W such that M, w |= ϕ. The empty initial memory ensures that no state
of the model satisfies the unary predicate k unless a formula r ψ has previously
been evaluated there.
Multimodal memory logic is shown to be undecidable in [7]. We strengthen

this result, showing that undecidability holds also in the monomodal case.
Theorem 1. The satisfiability problem of ML( r , k ) is undecidable.
Proof. The problem of concept consistency in the description logic ALCself is

undecidable [18]. Let us name Tiling(t) the concept defined in [18] that encodes
an instance t of the (undecidable) problem of tiling the plane. A reduction of
Tiling to the satisfiability problem of ML( r , k ) can be done by replacing the
ALCself operator ∀R by , ∃R by ♦, I by r and me by k .
We previously suggested that relation-changing operators could, each one in

its own way, simulate remember and known operators. However, there is one
important difference between the r operator and relation-changing operators
like sb. While sbϕ always results in a change in the model, r ϕ can leave the
memory unchanged if the current state of evaluation is already memorized. We
ignore this difference by observing that any ML( r , k )-formula can be rewritten
into an equivalent formula where every occurrence of r is “proper”, in the sense
that it actually modifies the memory.
Definition 6 (PNF). An ML( r , k )-formula is in proper normal form (PNF)

if every occurrence of a sub-formula r ψ occurs within the following sub-formula:
(¬ k ∧ r ψ) ∨ ( k ∧ ψ)
Finally, we define the notion of modal depth of an ML( r , k )-formula.
Definition 7. Given ϕ in ML( r , k ), we define the modal depth of ϕ (notation

mdϕ) as
md( k ) = 0
md(p) = 0 for p ∈ PROP
md( r ϕ) = md(ϕ)
md(¬ϕ) = md(ϕ)
md(ϕ ∧ ψ) = max{md(ϕ), md(ψ)}
md(♦ϕ) = 1 + md(ϕ).
In the next section we prove that the satisfiability problem of relation-

changing modal logics is undecidable via reductions from monomodal memory
logic. We assume that memory logic formulas are always in PNF. This is impor-
tant for structural inductive proofs.
6 C. Areces et al.
4 Undecidability of Relation-Changing Logics

In this section, we present satisfiability-preserving translations from ML( r , k )
to relation-changing modal logics. Combining these translations with the unde-
cidability result of Theorem 1, we can claim:
Theorem 2. The satisfiability problem of ML() is undecidable, for ∈ {sb,

br, sw, gsb, gbr, gsw}.
The main idea of these translations is to simulate the behavior of ML( r , k )

without having an external memory in the model. We simulate the ability to
store states in a memory by changing the accessibility relation of a model. Check-
ing for membership in the memory is simulated by checking for changes in the
accessibility relation.
Every translation τ from ML( r , k )-formulas to ML()-formulas proceeds
in two steps. For a given target logic, the translation includes a fixed part called
Struct , that enforces constraints on the structure of the model. The second part,
called Tr , is defined inductively on ML( r , k )-formulas, and uses the structure
provided by Struct to simulate the r and k operators.
Sabotage Logic
Local Sabotage. In the translation to local sabotage logic, the Structsb sub-
formula should ensure that every state of the model can be memorized using the
expressivity of sb. This operator changes the point of evaluation after deleting
an edge. To compensate for this, the Structsb formula guarantees that every
state has an edge that is deleted when the state is memorized, and a second edge
back to the original state to ensure that evaluation can continue at the correct
state. We use a spy point s to ensure this structure. The idea is illustrated in
the following image.
ϕ
...
s
We need to ensure that every satisfiable formula of ML( r , k ) is translated
into a satisfiable formula (and vice-versa, if the translated formula is satisfiable,
then the original formula is satisfiable, too). The image above shows an intended
model for the translated formula τsb (ϕ). Intuitively, bold edges and arrows
correspond to the model of ϕ. The complete translation is given in Definition 8.
Here we discuss in detail how it works.
Structsb adds a spy state with symmetric edges between itself and all other
states. In particular, (1) in Definition 8 ensures that the evaluation state satisfies
s and that it is irreflexive, and (2) guarantees that its immediate successors
reach a state where s holds. Formulas (3) and (4) ensure that this state is the
original s state. They work together as follows: (3) makes ♦s true in any s-
state reachable in two steps, and by deleting the traversed edges we avoid a cycle
of size two between this s-state and an immediate successor of the evaluation
state, distinguishing the original s-state from any other s-state reachable in two
steps. (4) then traverses one edge, deletes the next one, and reaches a state where
s implies ♦¬s. This contradicts (3), unless we have arrived in the original s
state. Formulas (5), (6) and (7) mimic (2), (3) and (4), but for edges which are
removed twice. Observe that (6) now avoids a cycle of size three between any
other s-state reachable in two steps and an immediate successor of the evaluation
state. Finally, (8) and (9) ensure that the evaluation state is indeed a spy state,
i.e., that it is linked to every other state of the input model.
Trsb starts by placing the translation ( ) of ϕ in a successor of the evaluation
state. Boolean cases are obvious. For the diamond case, ♦ψ is satisfied if there
is a successor v where ψ holds, but we must ensure that v is not the spy state.
For ( r ψ) , we do a round-trip of sabotaging from the current state to the spy
state. Note that after reaching the spy state an edge does come back to the same
state where it came from, since the only accessible state where ¬♦s holds is the
one we are memorizing. For ( k ) , we check whether there is an edge pointing to
some s-state.
Definition 8. Define τsb (ϕ) = Structsb ∧ Trsb (ϕ), where:
Structsb = s ∧ ¬s (1)

∧ ♦s (2)
∧ [sb][sb](s → ♦s) (3)
∧ [sb](s → ♦¬s) (4)
∧ (¬s → ♦s) (5)
∧ [sb](s→[sb](¬s→(s→♦s))) (6)
∧ [sb](s→(¬s→(s→♦¬s))) (7)
∧ (s → ♦s) (8)
∧ [sb](s → ♦¬s) (9)
Trsb (ϕ) = ♦(ϕ) , with:
(p) = p f or p ∈ PROP appearing in ϕ

( k ) = ¬♦s
(¬ψ) = ¬(ψ)
(ψ ∧ χ) = (ψ) ∧ (χ)
(♦ψ) = ♦(¬s ∧ (ψ) )
( r ψ) = sb(s ∧ sb(¬♦s ∧ (ψ) ))
Proposition 1. If W, R, V , w |= Structsb , then for every state v ∈ W \ {w}

there exists exactly one state v such that (v, v ), (v , v) ∈ R and v ∈ V (s).
Lemma 1. Let ϕ be an ML( r , k )-formula in PNF that does not contain the
propositional symbol s. Then, ϕ is satisfiable iff τsb (ϕ) is satisfiable.
8 C. Areces et al.
Proof. (⇐) Suppose W, R, V , s |= τsb (ϕ). Let W = W \V (s), R = R ∩ (W ×

W ) and V (p) = V (p) ∩ W for all p ∈ PROP. By definition of Trsb there is
w ∈ W such that (s, w ) ∈ R and W, R, V , w |= (ϕ) .
Now, let ψ be a sub-formula of ϕ, v ∈ W , S ⊆ W and RS = R\{(v, s), (s, v) |
v ∈ S}. We prove by structural induction on ψ that W , R , V , S, v |=
ψ if, and only if, W, RS , V , v |= (ψ) . In particular, this will prove that
W , R , V , ∅, w |= ϕ if, and only if, W, R, V , w |= (ϕ) .
The propositional, Boolean and modal cases are trivial. For ψ = k , we
should prove that W , R , V , S, v |= k if, and only if, W, RS , V , v |= ¬♦s.
However this is immediate by definition of S and RS and Proposition 1.
For the last case, consider ψ = ¬ k ∧ r χ (remember that formulas are
in PNP), so we should prove that W , R , V , S, v |= ¬ k ∧ r χ if, and only if,
W, RS , V , v |= ♦s∧sb(s∧sb(¬♦s∧(χ) . Again, the equivalence is immediate
by Proposition 1.
(⇒) Suppose W, R, V, ∅, w |= ϕ. We build a model for τsb (ϕ) by adding
the necessary parts to this model, that are, the spy state and the round-trip
paths. Define W , R , V as follows. Let s ∈ / W some state, W = W ∪{s}, R =
R∪{(x, s), (s, x) | x ∈ W }, V (s) = {s} and V (p) = V (p) for p ∈ PROP\{s}. By

construction, W , R , V , s |= Structsb , so Proposition 1 holds. We prove that

for all ψ sub-formula of ϕ, v ∈ W , S ⊆ W and RS = R \{(x, s), (s, x) | x ∈ S},
W, R, V, S, v |= ψ iff W , RS , V , v |= (ψ) . This can be done by structural
induction on ψ using Proposition 1. This proves that W, R, V, ∅, w |= ϕ iff
W , R , V , s |= τsb (ϕ), so τsb (ϕ) is satisfiable.
Global Sabotage. In [16] it is shown that multimodal sabotage logic is undecidable

via a reduction of the Post Correspondence Problem. The present proof extends
this result to the monomodal case via a reduction of the satisfiability problem
of the memory logic ML( r , k ). The notation i ϕ is defined as 0 ϕ = ϕ and
n+1 ϕ = n ϕ.
One piece of data needed to build τgsb (ϕ) is the modal depth of the input
formula (md(ϕ)). Up to the depth indicated by this value, Structgsb (ϕ) adds
to every state a transition to some state where s holds (In fact, this latter state
can be shared among several states of the input model.) It is as if each state
of the input model had a flag that could be turned on to identify the state.
Thus, remembering some state is simulated with Trgsb ( r ) by deleting the edge
between the state and its s-successor. For Trgsb ( k ), we check whether the
current state has an s-successor. The idea is illustrated in the following image.
s
s s
...
ϕ
Definition 9. Define τgsb (ϕ) = Structgsb (ϕ) ∧ Trgsb (ϕ), where:

Structgsb (ϕ) = ¬s ∧ i (¬s → ♦s)
0≤i≤md(ϕ)
Trgsb (p) = p f or p ∈ PROP appearing in ϕ

Trgsb ( k ) = ¬♦s
Trgsb (¬ψ) = ¬Trgsb (ψ)
Trgsb (ψ ∧ χ) = Trgsb (ψ) ∧ Trgsb (χ)
Trgsb (♦ψ) = ♦(¬s ∧ Trgsb (ψ))
Trgsb ( r ψ) = gsb(¬♦s ∧ Trgsb (ψ))
Proposition 2. Let dist(a, b) the minimal number of R-steps to reach some

state b from some state a. Let ϕ some memory logic formula. If W, R, V , w |=
Structgsb (ϕ), then for all x ∈ W such that dist(w, x) ≤ md(ϕ), x has a succes-
sor where s holds.
Proposition 3. If W, R, V , w |= ♦s ∧ gsb¬♦s, then w has one and only one

successor where s holds.
propositional symbol s. Then, ϕ is satisfiable iff τgsb (ϕ) is satisfiable.
Proof. (⇐) Suppose W, R, V , w |= τgsb (ϕ). Let W = W \V (s), R = R∩(W ×

W ), and V (p) = V (p) ∩ W for p ∈ PROP \ {s}. We should prove that for all ψ
sub-formula of ϕ of modal depth md(ψ) ≤ md(ϕ) − dist(w, v), v ∈ W accessible
from w within md(ϕ) steps, S ⊆ W , and RS = R \ {(x, y) | |x ∈ S, y ∈ V (s)},
then W , R , V , S, v |= ψ iff W, RS , V , v |= Trgsb (ψ).
The proof is by structural induction on ψ. The non-memory cases are easy.
For the k case, we should show that W , R , V , S, v |= k iff W, RS , V , v |=
¬♦s, this is immediate by Proposition 2 and the definitions of S and RS .
Then for the remaining case, we have to show that W , R , V , S, v |= ¬ k ∧
r χ iff W, RS , V , v |= ♦s ∧ gsb(¬♦s ∧ Trgsb (χ)), which can be proved using
the definition of |=, IH and Proposition 3.
(⇒) Suppose W, R, V, ∅, w |= ϕ. Let s ∈ / W . Define W , R , V , where
W = W ∪{s}, R = R∪{(v, s) | v ∈ W }, V (s) = {s}, and V (p) = V (p), for p ∈

PROP appearing in ϕ. It is easy to check that W , R , V , w |= Structgsb (ϕ),

hence Proposition 2 holds. Then, let us prove that for all ψ sub-formula of ϕ
of modal depth md(ψ) ≤ md(ϕ) − dist(w, v), v ∈ W accessible from w within
md(ϕ) steps, S ⊆ W and RS = R \ {(x, s) | x ∈ S}, we have the equivalence
W, R, V, S, v |= ψ iff W , RS , V , v |= Trgsb (ψ). This is done by structural
induction on ψ. For the case k the equivalence is immediate, and for the case
¬ k ∧ r χ, Proposition 3 provides the equivalence needed.
Bridge Logic
Local Bridge. For local bridge logic, we use a spy state that is initially discon-
nected from the input model. When some state should be memorized, the spy
state gets connected (in both directions) to it. This construction is quite special
since we do not have pre-built gadgets in the input model, as they get built on
demand.
10 C. Areces et al.
Let us first show the following result, that enables us to force the evaluation
state to be the only one in the model to satisfy s:
Lemma 3. Let ϕ = s ∧ ⊥ ∧ [br](s→[br]¬s). If M, w |= ϕ, then w is the only

state in the model M where s holds.
Proof. First, w obviously satisfies s and does not have any successor. Now, we
have M, w |= [br](s→[br]¬s). In particular this means that M+ ww , w |= s→[br]¬s,
hence M+ ww , w |= [br]¬s. Since in M +
ww , the state w is only connected to itself,
this means that for all v = w, we have M+ ww,wv , v |= ¬s, this also means that
M, v |= s for all v = w.
For Bridge Logics, Structbr adds to the input model a spy state in which s
holds. By Lemma 3, (1) in Definition 10 ensures that the evaluation state has
no successor and is the only state in the model where s holds. And (2) ensures
that there are no edges from ¬s-states (anywhere in the model) to the spy state.
The idea is illustrated in the following image, where t is a propositional symbol
used in Trbr (ϕ) and dotted lines represent edges created with the br operator.
t ...
ϕ
Definition 10. Define τbr (ϕ) = Structbr ∧ Trbr (ϕ), where:
Structbr = s ∧ ⊥ ∧ [br](s→[br]¬s) (1)

∧ [br](¬s → ¬s) (2)
Trbr (ϕ) = br(¬s ∧ t ∧ br(¬s ∧ ¬t ∧ (ϕ) )), with:

( k ) = ♦s
(¬ψ) = ¬(ψ)
(ψ ∧ χ) = (ψ) ∧ (χ)
(♦ψ) = ♦(¬s ∧ ¬t ∧ (ψ) )
( r ψ) = br(s ∧ br(¬s ∧ ♦s ∧ (ψ) ))
Trbr (ϕ) first creates two edges until a ¬s-state, where the translation of ϕ
holds. For Trbr ( r ) we do a round-trip of bridging from the current state to
the spy state. Note that the second part of this round-trip has to be from the
spy state to the remembered state, since it is the only way to satisfy br(♦s).
Also note that this would not work if the s state was directly connected to the
input model; this is why we use the intermediate t-state. For Trbr ( k ) we check
whether there is an edge to a state where s holds.
Proposition 4. Let W, R, V a model such that there is a unique state s where
s holds, there is no state x ∈ W such that (x, s) ∈ R, and there is a component
C ⊆ W such that s ∈ / C and for all y ∈ C, (s, y) ∈

/ R. Let S ⊆ C and RS =
R ∪ {(x, s), (s, x) | x ∈ S}.
Then in the model W, RS , V , evaluating the formula br(s∧br♦s) at some
state y ∈ C \ S changes the evaluation state to s, then again to the same state
y adding the edges (y, s) and (s, y) to the relation.
propositional symbols s and t. Then, ϕ is satisfiable iff τbr (ϕ) is satisfiable.
Proof. (⇐) Suppose W, R, V , s |= τbr (ϕ). Define M = W , R , V , ∅ with

W = (W \ V (s)) \ V (t), R = R ∩ (W × W ), and V (p) = V (p) ∩ W for
all p ∈ PROP. By definition of Trbr there is w ∈ W such that s = w and
W, R, V , w |= (ϕ) .
Let ψ a sub-formula of ϕ, v ∈ W , S ⊆ W , and RS = R ∪ {(x, s), (x, v) | x ∈
S}, then we will prove that W , R , V , S, v |= ψ iff W, RS , V , v |= (ψ) .
We prove it by structural induction on ψ. For the ¬ k ∧ r χ case, suppose
W , R , V , S, v |= ¬ k ∧ r χ. By definition, this is equivalent to W , R , V , S ∪
{v}, v |= χ with v ∈ / S, Then, by definition of RS and inductive hypothesis

we get W, (RS )+ {(v,s),(s,v)} , V , s |= (χ) , with (v, s) ∈
/ RS and (s, v) ∈
/ RS . By
Proposition 4, this is equivalent to W, RS , V , v |= ¬♦s∧br(s∧br(♦s∧(χ) )).
thus we have W, RS , V , v |= (¬ k ∧ r χ) .
(⇒) Suppose W, R, V, ∅, w |= ϕ. Let s, t ∈ / W . Define M = W , R, V
such that W = W ∪ {s, t}, V (s) = {s}, V (t) = {t} and V (p) = V (p) for

p ∈ PROP appearing in ϕ. We can easily check that W , R, V , s |= Structbr ,

and we can also check by structural induction on ϕ that W, R, V, S, w |= ϕ iff
W , RS , V , s |= Trbr (ϕ), where RS = R ∪ {(v, s), (s, v) | v ∈ S}.
Global Bridge. The global bridge operator is able to add edges in the model.
This is why, to mark some state, we use this operator to add an edge to some
s-state. Then, we enforce that the initial model does not have any reachable
s-state.
Here Structgbr (ϕ) ensures that no state of the input model has s-successors.
Storing a state in the memory is simulated by creating an edge to an s-state, and
checking whether the current state of evaluation is in the memory is simulated
by checking the presence of an s-successor. Observe that we could have either
one state where s holds or (possibly) different s-states for each state of the input
model.
s
...
ϕ
12 C. Areces et al.
Definition 11. Define τgbr (ϕ) = Structgbr (ϕ) ∧ Trgbr (ϕ), where:

Structgbr (ϕ) = i ¬s
0≤i≤md(ϕ)+1
Trgbr (p) = p f or p ∈ PROP appearing in ϕ

Trgbr ( k ) = ♦s
Trgbr (¬ψ) = ¬Trgbr (ψ)
Trgbr (ψ ∧ χ) = Trgbr (ψ) ∧ Trgbr (χ)
Trgbr (♦ψ) = ♦(¬s ∧ Trgbr (ψ))
Trgbr ( r ψ) = gbr(♦s ∧ Trgbr (ψ))
propositional symbol s. Then, ϕ is satisfiable iff τgbr (ϕ) is satisfiable.
Swap Logic
Local Swap. We introduce a new version of the translation given in [4] that uses
only one propositional symbol. The idea is that we have each state pointing
to some states called switch states, and memorizing a state is represented by
swapping such edges. Then, no edge pointing to a switch
means that the state
has been memorized. We use the notation (n) ϕ for i ϕ.
1≤i≤n
In this case Structsw adds “switch states”, which are in one-to-one corre-
spondence with the states of the input model, together with a spy state. By (2)
in Definition 12, each ¬s-state at one, two and three steps from the evaluation
state, has a unique dead-end successor where s holds (switch state). By (3) and
(4), switch states (corresponding to states at distance 1, 2 and 3) can be reached
from the evaluation state by a unique path. (5) makes the evaluation state a spy
state. All these conjuncts together ensure that switch states are independent one
from another. The idea is illustrated in the following image.
s
s s
...
ϕ
s
Definition 12. Define τsw = Structsw ∧ Trsw (ϕ), where:
Structsw =
s ∧ ¬s (1)
∧ (3) (¬s → U niq) (2)
∧ [sw](s → (s → ⊥) (3)
∧ [sw](s → (s → ⊥) (4)
∧ [sw][sw](¬s→sw(s ∧ ♦((¬s)→♦♦(s ∧ ♦¬♦s)))) (5)
U niq = ♦(s ∧ ⊥) ∧ [sw](s → ¬♦s)

Trsw (ϕ) = ♦(ϕ) , with:

( k ) = ¬♦s
(¬ψ) = ¬(ψ)
(ψ ∧ χ) = (ψ) ∧ (χ)
(♦ψ) = ♦(¬s ∧ (ψ) )
( r ψ) = sw(s ∧ ♦(ψ) )
For Trsw ( r ϕ) we traverse and swap the edge between the current state
and its switch state, and come back to the same state. For Trsw ( k ), we check
whether the current state has not an edge to its switch state.
Proposition 5. Let W, R, V , s |= Structsw , W = W \ V (s) and S ⊆ W .

Then T = {(v , v) | v ∈ S ∧ (v, v ) ∈ R ∧ v ∈ V (s)} is a bijection.
propositional symbol s. Then, ϕ is satisfiable iff τsw (ϕ) is satisfiable.
Proof. (⇐) From a pointed model W, R, V , w of τsw (ϕ) we can extract a
pointed model W , R , V , ∅, w satisfying ϕ following the same definition as in
the proof of Lemma 1.
For all ψ sub-formula of ϕ, v ∈ W , S ⊆ W , T = {(v , v) | v ∈ S ∧ (v, v ) ∈
R ∧ v ∈ V (s)} and RS = (R\T −1 ) ∪ T , we will prove that W , R , V , S, v |= ψ
if, and only if, W, RS , V , v |= (ψ) .
We do it by structural induction on ψ. We prove the ¬ k ∧ r χ case. Suppose
W , R , V , S, v |= ¬ k ∧ r χ. Then by definition, v ∈ / S and W , R , V , S ∪
{v}, v |= χ, and by Proposition 5, we have (v, v ) ∈ RS for a unique v ∈ V (s).

Then, by definition of RS and inductive hypothesis we get W, (RS )∗v v , V , v |=

(χ) . By definition of |= and by Proposition 5, W, (RS )∗v v , V , v |= s ∧ ♦(χ) ,
and again, W, RS , V , v |= ♦s ∧ sw(s ∧ ♦(χ) ), thus we have, equivalently,
W, RS , V , v |= (¬ k ∧ r χ) .
(⇒) Suppose W, R, V, ∅, w |= ϕ. Let sw be a bijective function between W
and a set U such that U ∩ W = ∅, and s ∈ / U ∪ W . Define M = W , R , V

such that W = W ∪ {s} ∪ U , R = R ∪ {(s, w) | w ∈ W } ∪ {(w, sw(w)) | w ∈
W }, V (s) = {s} ∪ U , and V (p) = V (p) for p ∈ PROP appearing in ϕ. It
is easy to check that W , R , V , s |= Structsw , in particular, Proposition 5
is relevant. Then, we can easily prove that for all ψ sub-formula of ϕ, v ∈
W , S ⊆ W , T = {(sw(v), v) | v ∈ S} and RS = (R \T −1 ) ∪ T , we have
the equivalence W, R, V, S, v |= ψ iff W , RS , V , v |= (ψ) . This is done by
structural induction on ψ.
Global Swap. The global swap operator is able to change the direction of some
edge in the model. In particular, we are interested in the ability to swap, for
some state, an incoming edge (undetectable for the basic modal logic) into an
outgoing edge. This is why this translation is similar to the one of global bridge
logic. Initially, the model does not have any reachable state where s holds. As
14 C. Areces et al.
for global sabotage and global bridge, there may be many states where s holds
in the model with edges to states of the input model. The idea is illustrated in
the following image, where only one s state is shown.
s
...
ϕ
Definition 13. Define τgsw (ϕ) = Structgsw (ϕ) ∧ Trgsw (ϕ), where:

Structgsw (ϕ) = i ¬s
0≤i≤md(ϕ)+1
Trgsw (p) = p f or p ∈ PROP appearing in ϕ

Trgsw ( k ) = ♦s
Trgsw (¬ψ) = ¬Trgsw (ψ)
Trgsw (ψ ∧ χ) = Trgsw (ψ) ∧ Trgsw (χ)
Trgsw (♦ψ) = ♦(¬s ∧ Trgsw (ψ))
Trgsw ( r ψ) = gsw(♦s ∧ Trgsw (ψ))
Proposition 6. Let W, R, V , w |= ¬♦s ∧ gsw♦s. Then, by the semantics of

the global swap operator, there exists a state v ∈ W \ {w} such that (v, w) ∈ R
and v ∈ V (s).
propositional symbol s. Then, ϕ is satisfiable iff τgsw (ϕ) is satisfiable.
5 Conclusions
We exploited the similarities between memory logic and relation-changing logics
to obtain simple and non-redundant undecidability proofs. We first presented an
undecidability result for memory logics in the monomodal case, by adapting the
proof introduced in [18] for ALCself. Then, we presented translations from the
satisfiability problem of monomodal memory logics to all six relation-changing
modal logics. Both results combined show undecidability of the satisfiability
problem for relation-changing modal logics in a very simple way. These results
complete the picture of the computational behaviour of relation-changing logics,
given that we already know that model checking for them is PSPACE-complete
[2,4,5,15].
This high complexity of the logics is a consequence of the degree of liberty
we give to the operators. By replacing arbitrary modifications with conditional
modifications (i.e., according to a pre- and a post-condition) it is possible to
decrease the complexity and get decidable logics (e.g., as in [9,10]).
A related problem is the one of finite satisfiability. Indeed, for many applica-
tions of dynamic epistemic logic, we are only interested in looking for finite mod-
els. Finite satisfiability is known to be undecidable for multimodal global
sabotage logic [20], and decidable for monomodal local sabotage and local swap
logics [6]. It remains to see the status of this problem for all remaining cases.
Acknowledgements. This work was partially supported by grant ANPCyT-PICT-

2013-2011, STIC-AmSud “Foundations of Graph Structured Data (FoG)”, SeCyT-
UNC, the Laboratoire International Associé “INFINIS”, and the EU Horizon 2020
research and innovation programme under the Marie Skodowska-Curie grant No.
690974, project MIREL: MIning and REasoning with Legal texts.
References
1. Areces, C.: Hybrid logics: the old and the new. In: Proceedings of LogKCA 2007,
pp. 15–29 (2007)
2. Areces, C., Fervari, R., Hoffmann, G.: Moving arrows and four model checking
results. In: Ong, L., de Queiroz, R. (eds.) WoLLIC 2012. LNCS, vol. 7456, pp. 142–
153. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32621-9 11
3. Areces, C., Fervari, R., Hoffmann, G.: Tableaux for relation-changing modal logics.
In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI),
vol. 8152, pp. 263–278. Springer, Heidelberg (2013). https://doi.org/10.1007/978-
3-642-40885-4 19
4. Areces, C., Fervari, R., Hoffmann, G.: Swap logic. Logic J. IGPL 22(2), 309–332
(2014)
5. Areces, C., Fervari, R., Hoffmann, G.: Relation-changing modal operators. Logic
J. IGPL 23(4), 601–627 (2015)
6. Areces, C., Fervari, R., Hoffmann, G., Martel, M.: Relation-changing logics as
fragments of hybrid logics. In: Cantone, D., Delzanno, G. (eds.) Proceedings of
the Seventh International Symposium on Games, Automata, Logics and Formal
Verification, GandALF 2016, Italy. EPTCS, vol. 226, pp. 16–29 (2016)
7. Areces, C., Figueira, D., Figueira, S., Mera, S.: The expressive power of memory
logics. Rev. Symb. Logic 4(2), 290–318 (2011)
8. Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem,
J. (eds.) Handbook of Modal Logic, pp. 821–868. Elsevier (2007)
9. Areces, C., van Ditmarsch, H., Fervari, R., Schwarzentruber, F.: Logics with copy
and remove. In: Kohlenbach, U., Barceló, P., de Queiroz, R. (eds.) WoLLIC 2014.
LNCS, vol. 8652, pp. 51–65. Springer, Heidelberg (2014). https://doi.org/10.1007/
978-3-662-44145-9 4
10. Areces, C., van Ditmarsch, H., Fervari, R., Schwarzentruber, F.: The modal logic
of copy and remove. To Appear in Information and Computation (2015). Special
Issue of WoLLIC 2014
11. Aucher, G., Schwarzentruber, F.: On the complexity of dynamic epistemic logic.
In: Proceedings of TARK 2013, Chennai, India, January 2013
12. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in The-
oretical Computer Science. Cambridge University Press, New York (2001)
13. Blackburn, P., Seligman, J.: Hybrid languages. J. Logic Lang. Inf. 4(3), 251–272
(1995)
16 C. Areces et al.
14. Blackburn, P., van Benthem, J.: Modal logic: a semantic perspective. In: Handbook
of Modal Logic, pp. 1–84. Elsevier (2007)
15. Fervari, R.: Relation-Changing Modal Logics. Ph.D. thesis, Universidad Nacional
de Córdoba, Argentina (2014)
16. Löding, C., Rohde, P.: Model checking and satisfiability for sabotage modal logic.
In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp.
302–313. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-24597-
1 26
17. Lutz, C.: Complexity and succinctness of public announcement logic. In: Proceed-
ings of the 5th International Joint Conference on Autonomous Agents and Multi-
agent Systems, AAMAS 2006, New York, NY, USA, pp. 137–143 (2006)
18. Marx, M.: Narcissists, stepmothers and spies. In: Proceedings of DL 2002, vol. 53.
CEUR (2002)
19. Mera, S.: Modal memory logics. Ph.D. thesis, Université Henri Poincaré, Nancy,
France and Universidad de Buenos Aires, Argentina (2009)
20. Rohde, P.: On games and logics over dynamically changing structures. Ph.D. thesis,
RWTH Aachen (2006)
21. Benthem, J.: An essay on sabotage and obstruction. In: Hutter, D., Stephan, W.
(eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol. 2605, pp. 268–276.
Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32254-2 16
22. van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic. Synthese
Library. Springer, Dordrecht (2007). https://doi.org/10.1007/978-1-4020-5839-4
Axiomatization and Computability of a Variant
of Iteration-Free P DL with Fork
Philippe Balbiani(B) and Joseph Boudou
Institut de recherche en informatique de Toulouse,

CNRS — Université de Toulouse, 118 route de Narbonne,
31062 Toulouse Cedex 9, France
Philippe.Balbiani@irit.fr
Abstract. We devote this paper to the axiomatization and the com-

putability of P DLΔ
0 —a variant of iteration-free P DL with fork.
Keywords: Iteration-free P DL · Fork · Axiomatization

Computability
1 Introduction
Propositional dynamic logic (P DL) is an applied non-classical logic designed
for reasoning about the behaviour of programs [10]. The definition of its syntax
is based on the idea of associating with each program α of some programming
language the modal operator [α], formulas of the form [α]φ being read “every
execution of the program α from the present state leads to a state bearing
the formula φ”. Completeness and decidability results for the standard version
of P DL in which programs are built up from program variables and tests by
means of the operations of composition, union and iteration are given in [15,16].
A number of interesting variants have been obtained by extending or restricting
the syntax or the semantics of P DL in different ways [7,9,14,18].
Some of these variants extend the ordinary semantics of P DL by considering
sets W of states structured by means of a function from the set of all pairs of
states into the set of all states [5,11–13]: the state x is the result of applying the
function to the states y, z iff the information concerning x can be separated in
a first part concerning y and a second part concerning z. The binary function
considered in [5,11] has its origin in the addition of an extra binary operation of
fork denoted ∇ in relation algebras: in [5, Sect. 2], whenever x and y are related
via R and z and t are related via S, states in x z and states in y t are related
via R∇S whereas in [11, Chap. 1], whenever x and y are related via R and x
and z are related via S, x and states in y z are related via R∇S.
This addition of fork in relation algebras gives rise to a variant of P DL
which includes the program operation of fork denoted Δ. In this variant, for all
programs α and β, one can use the modal operator [αΔβ], formulas of the form
[αΔβ]φ being read “every execution in parallel of the programs α and β from the
c Springer International Publishing AG 2018
A. Madeira and M. Benevides (Eds.): DALI 2017, LNCS 10669, pp. 17–34, 2018.
https://doi.org/10.1007/978-3-319-73579-5_2
18 P. Balbiani and J. Boudou
present state leads to a state bearing the formula φ”. The binary operation of
fork ∇ considered in Benevides et al. [5, Sect. 2] gives rise to P RSP DL, a variant
of P DL with fork whose axiomatization is still open. We devote this paper to
the axiomatization and the computability of P DLΔ 0 , a variant of iteration-free
P DL with fork whose semantics is based on the interpretation of the binary
operation of fork ∇ considered in Frias [11, Chap. 1].
The difficulty in axiomatizing or deciding P RSP DL or P DLΔ 0 originates in
the fact that the program operations of fork considered above are not modally
definable in the ordinary language of P DL. We overcome this difficulty by means
of tools and techniques developed in [1,3,4]. Our results are based on the fol-
lowing: although fork is not modally definable, it becomes definable in a modal
language strengthened by the introduction of propositional quantifiers. Instead
of using axioms to define the program operation of fork in the language of P DL
enlarged with propositional quantifiers, we add an unorthodox rule of proof that
makes the canonical model standard for the program operation of fork and we
use large programs for the proof of the Truth Lemma.
We will first present the syntax (Sect. 2) and the semantics (Sect. 3) of P DLΔ 0
and continue with results concerning the expressivity of P DLΔ 0 (Sect. 4), the
axiomatization/completeness of P DLΔ 0 (Sects. 5 and 6) and the decidability of
P DLΔ 0 (Sect. 7). We assume the reader is at home with tools and techniques in
modal logic and dynamic logic. For more on this, see [6,15]. The proofs of our
results can be found in [2].
2 Syntax
This section presents the syntax of P DLΔ

0 . As usual, we will follow the standard
rules for omission of the parentheses.
Definition 1 (Programs and formulas). The set P RG of all programs and

the set F RM of all formulas are inductively defined as follows:
– α, β ::= a | (α; β) | (αΔβ) | φ?;

– φ, ψ ::= p | ⊥ | ¬φ | (φ ∨ ψ) | [α]φ | (φ ◦ ψ) | (φ ψ) | (φ ψ);
where a ranges over a countably infinite set of program variables and p ranges
over a countably infinite set of propositional variables.
We will use α, β, . . . for programs and φ, ψ, . . . for formulas. The Boolean

constructs for formulas are defined as usual. A number of other constructs for
formulas can be defined in terms of the primitive ones as follows.
Definition 2 (Abbreviations). The modal constructs for formulas ··, (·¯ ◦·),
(·¯·) and (·¯·) are defined as follows: αφ ::= ¬[α]¬φ; (φ¯
◦ψ) ::= ¬(¬φ ◦ ¬ψ);
(φ¯ψ) ::= ¬(¬φ ¬ψ); (φ¯ψ) ::= ¬(¬φ ¬ψ). Moreover, for all formulas φ, let
φ0 ::= ¬φ and φ1 ::= φ.
Axiomatization and Computability of a Variant of Iteration-Free PDL 19
It is well worth noting that programs and formulas are finite strings of sym-
bols coming from a countable alphabet. It follows that there are countably many
programs and countably many formulas. The construct ·; · comes from the class
of algebras of binary relations [19]: the program α; β firstly executes α and sec-
ondly executes β. As for the construct ·Δ·, it comes from the class of proper fork
algebras [11, Chap. 1]: the program αΔβ performs a kind of parallel execution
of α and β. The construct [·]· comes from the language of P DL [10,15]: the for-
mula [α]φ says that “every execution of α from the present state leads to a state
bearing the information φ”. As for the constructs · ◦ ·, · · and · ·, they come
from the language of conjugated arrow logic [8,17]: the formula φ ◦ ψ says that
“the present state is a combination of states bearing the information φ and ψ”,
the formula φ ψ says that “the present state can be combined to its left with a
state bearing the information φ giving us a state bearing the information ψ” and
the formula φ ψ says that “the present state can be combined to its right with
a state bearing the information ψ giving us a state bearing the information φ”.
Example 1. The formula [aΔb](p ◦ q) says that “the parallel execution of a and
b from the present state always leads to a state resulting from the combination
of states bearing the information p and q”.
Obviously, programs are built up from program variables and tests by

means of the constructs ·; · and ·Δ·. Let α(φ1 ?, . . . , φn ?) be a program with
(φ1 ?, . . . , φn ?) a sequence of some of its tests. The result of the replacement of
φ1 ?, . . . , φn ? in their places with other tests ψ1 ?, . . . , ψn ? is another program
which will be denoted α(ψ1 ?, . . . , ψn ?). Now, we introduce the function f from
the set of all programs into itself defined as follows.
Definition 3 (Test insertion). Let f be the function from the set of all pro-
grams into itself inductively defined as follows:
– f (a) = a;
– f (α; β) = f (α); ?; f (β);
– f (αΔβ) = (f (α); ?)Δ(f (β); ?);
– f (φ?) = φ?.
Example 2. If α = aΔb, f (α) = (a; ?)Δ(b; ?).
Now, we introduce parametrized actions and admissible forms.
Definition 4 (Parametrized actions and admissible forms). The set

P AR of all parametrized actions and the set ADM of all admissible forms are
inductively defined as follows:
– ᾰ, β̆ ::= (ᾰ; β) | (α; β̆) | (ᾰΔβ) | (αΔβ̆) | ¬φ̆?;

– φ̆, ψ̆ ::= | [ᾰ]⊥ | (φ̆¯◦ψ) | (φ¯◦ψ̆) | (φ̆¯ψ) | (φ¯
ψ̆) | (φ̆¯ψ) | (φ¯ψ̆);
where is a new propositional variable, α, β range over P RG and φ, ψ range

over F RM .
Another random document with
no related content on Scribd:
Sketches of the Manners, Customs, and History
of the Indians of
America.
CHAPTER IV.
Discovery of the Pacific Ocean.—Plans of Columbus.—Avarice of
the Spaniards.—Balboa.—Weighing the gold.—The young
Indian’s speech.—Indian mode of fighting.—Balboa ascends
the mountain.—First view of the Pacific.
Columbus had first seen land in the New World on the 12th of
October, 1492. Six years after he surveyed the coast of the
American continent by Paria and Cumana. Territory was the grand
object with the noble mind of Columbus; he wished to colonize this
great country by the settling of Europeans, and thus introduce
Christianity and civilization among the Red Men. But the adventurers
that followed him sought gold as their only object, and employed the
sword as the only means of converting the natives.
The Spaniards who first landed on the continent, saw before them
a magnificent country, vast forests, mighty rivers, long ranges of
mountains—a dominion wide enough for the widest ambition of
conquest, or the richest enjoyment of life; but no treasure. Still their
avarice was kept in a perpetual fever by the Indian stories of gold in
profusion farther to the west, and their fancy was excited by tales of
a sea beyond, which they said stretched to the extremities of the
globe.
The first European who set his eye on the Pacific Ocean, was
Vasco Thenez De Balboa. His family was of the order of Spanish
gentry. He was a man of great enterprise, personal strength, and of a
daring courage. He had been disappointed in his expectations of
obtaining wealth at Hayti, where he had settled, and an expedition
sailing to Darien, he accompanied it. A colony was already
established on the eastern side of the isthmus of Darien; but the
savages in the vicinity had been found so warlike, that the settlers
did not venture to explore the interior.
Indian rumors of the golden country continued to inflame the
Spaniards. They heard of one king Dabaibe, who was said to be
living in a city filled with treasure, and who worshipped an idol of
solid gold. Balboa put himself at the head of his countrymen, and
marched to conquer the rich city. But they had first to conquer the
surrounding caciques, who would not permit the Spaniards to pass
through their territories. At length, Balboa formed an alliance with
Comogre, a mountain chieftain, who had three thousand warriors.
The son of Comogre brought a present to the Spanish troops of
sixty slaves and four thousand pieces of gold. In distributing the gold,
some difficulty occurred, as is usually the case where people are all
selfish; the quarrel grew furious, and swords were drawn. The young
Indian looked on, first with astonishment, then with scorn. Advancing
to the scales in which they were weighing the gold, he threw them on
the ground, exclaiming—“Is it for this trifle that you Spaniards
quarrel? If you care for gold, go seek it where it grows. I can show
you a land where you may gather it by handfuls.”
This speech brought all the Spaniards around him, and he
proceeded to detail his knowledge. “A cacique, very rich in gold,”
said he, “lives to the south, six suns off.” He pointed in that direction.
“There,” said he, “you will find the sea. But there you will find ships
as large as your own, with sails and oars. The men of these lands
are so rich, that their common eating and drinking vessels are of
gold.” This was to the Spaniards their first knowledge of Peru.
Balboa determined to search for this rich country. He collected a
hundred and ninety Spanish soldiers, a thousand friendly Indians,
and some bloodhounds, and began his march into the wilderness.
The Indian tribes were instantly roused. The Spaniards had scarcely
reached the foot of the Sierra, when they found the warriors, headed
by their caciques, drawn up in a little army.
The Indians, like the ancient Greeks, first defied the enemy, by
loud reproaches and expressions of scorn. They then commenced
the engagement. Torecha, their king, stood forth in the front of his
people, clothed in a regal mantle, and gave the word of attack. The
Indians rushed on with shouts; but the Spanish crossbows and
muskets were terrible weapons to their naked courage. The Indians
were met by a shower of arrows and balls, which threw them into
confusion. They were terrified, also, at the noise of the guns. They
thought the Spaniards fought with thunder and lightning. Still, the
Indians did not fly till their heroic king and six hundred of their
warriors were left dead on the spot. Over their bleeding bodies,
Balboa marched to the plunder of their city.
Balboa, with his army, now commenced the ascent of the
mountains. It took them twenty days. After toiling through forests,
and climbing mountains that seemed inaccessible, his Indian guide
pointed out to him, among the misty summits of the hills that lay
before him, the one from which the Pacific was visible. Balboa
determined to have the glory of looking upon it first. He commanded
his troops to halt at the foot of the hill. He ascended alone, with his
sword drawn, and having reached the summit, cast his eyes around.
The Pacific Ocean was spread out before him!
Balboa had invaded the Indian country in search of gold, and
murdered the natives to obtain it; but at that time such conduct was
not considered very wicked. The Indians were looked upon with
horror, because they were savages, and Balboa believed himself a
good Christian because he was a Catholic. He fell on his knees, and,
weeping, offered his thanksgiving to Heaven, for the bounty that had
suffered him to see this glorious sight. He doubtless thought God
was well pleased with him.
His troops had watched his ascent of the mountain, with the
eagerness of men who felt their fates bound up in his success. When
they saw his gestures of delight and wonder, followed by his falling
on his knees and prayer, they became incapable of all restraint. They
rushed up the hill like wild deer. But when they saw the matchless
prospect around them, they, too, shared the spirit of their leader;
they fell on their knees and offered up their thanksgiving to God. Yet
at the same time they doubtless contemplated plundering and
destroying the Indians. They had not learned to do to others as they
would have others do to them.
Lion Hunting.
Most people are more disposed to run away from lions than to
run after them, unless indeed they are safely locked up in cages. But
only think of going to hunt lions in the wilderness! Yet such things are
done in Africa, where lions are frequently met with.
In the southern part of that country is a tribe of negroes called the
Bechuana. The men of this tribe are accustomed to carry a long staff
with a bunch of ostrich feathers tied at one end, which is used to
shade themselves from the sun. It is in fact a kind of parasol, but
whether it is designed to save their complexion, I cannot say. It
seems, at any rate, that the ladies do not use it. But beside serving
as a parasol, this feathered staff has another and important use. As I
have said, these people sometimes go in pursuit of the lion, and
when a party of hunters meet one, they go near to him, and as he
springs on one of them, the hunter quickly plants the handle of the
staff in the ground and retreats. The fierce lion leaps upon the staff
and rends the ostrich feathers in pieces. While he is thus engaged,
the other hunters come suddenly upon him from behind, and
despatch him with their daggers.
“Isn’t your hat sleepy?” inquired a little urchin of a man with a

shocking bad one on. “No; why?” inquired the gentleman. “Why,
because it looks as if it was a long time since it had a nap.”
Merry’s Life and Adventures.
CHAPTER IX.
Completion of my education.—Manly sports.—An accident.—The
bed of pain.—Recovery from sickness.—A new companion.
In the last chapter I have given an account of a day in spring. I

might now proceed to relate the adventures and amusements of a
day in summer, then of autumn, and lastly of winter; and each of
these, it would appear, had its appropriate occupations and
diversions. But I am afraid that I shall weary my readers with long
stories. I shall therefore proceed with matters more immediately
affecting my fortunes, and tending to get to the end of a long journey.
I must go forward to the period when I was about sixteen years of
age, and when I had finally taken leave of the school. I had passed
through the branches taught there at the time; but these were few, as
I have already stated, and I was far from having thoroughly mastered
even them. I had, in fact, adopted a habit of skimming and slipping
along, really learning as little as possible. Not only was I indulged by
my uncle and his household, but there was a similar system of
tolerance extended toward my faults and follies, even by the
schoolmaster. It is true that sometimes he treated me harshly
enough; but it was generally in some fit of spleen. If he was gloomy
and tyrannical to the school, he was usually lenient to me. He even
excused my indolence, and winked at my neglect of study and duty.
It would seem that such general favor, should cultivate in the
heart of a youth only kind and generous feelings; but it was not so
with me. The more I was indulged, the more passionate and
headstrong I grew; and perhaps, in this, I was not unlike other young
people. It seems that there are wild passions in our very nature,
which are like weeds, ever tending to overgrow the whole soil. These
passions need to be eradicated by constant care and correction, just
as weeds must be pulled up by the roots and thrown away. Of what
use is it to plant a garden, if you do not hoe it and rake it, thus
keeping the weeds down, and allowing the proper plants to flourish?
And of what advantage is it to go to school, to be educated, if the
thorns and briers of vice and passion are not destroyed, and the
fruits and flowers of truth and virtue cultivated and cherished?
Being no more a school-boy, I now thought myself a man. Bill
Keeler had left my uncle, and was apprenticed to a shoemaker; but
in the evening I often contrived to meet him, and one or two other
companions. Our amusements were not such as would tell well in a
book. Too often we went to the bar-room of my uncle’s inn, and
listened to the vulgar jokes and coarse fun that were always stirring
there, and sometimes we treated each other with liquor. I cannot now
but wonder that such things should have given me any pleasure; but
habit and example have a mighty influence over us. Seeing that
others drank, we drank too, though at first the taste of all spirits was
odious to me. I got used to it by degrees, and at last began to like
the excitement they produced. And strange to say, the bar-room,
which originally disgusted me, became rather a favorite place of
resort. I was shocked at the oaths and indecency for a time; the
huge puddles of tobacco spittle over the floor, and the reeking flavors
of tobacco smoke and brandy, disgusted me; the ragged, red-nosed
loungers of the place, the noise, the riot, the brutality, which
frequently broke out, and which was called by the soakers, having a
“good time,” were actually revolting; but my aversion passed away
by degrees. Under the strong infection of the place, I partially
adopted its habits; I learned to smoke and chew tobacco, though
several fits of nervous sickness warned me of the violence I was
doing to my nature. I even ventured to swear occasionally; and, if the
truth must be told, I followed out, in various ways, the bad lessons
that I learnt.
It is painful to me to confess these things, but I do it for the
purpose of warning those for whose benefit I write, against similar
errors. Wherever young people go frequently, there they are learning
something; and as a bar-room is a place to which young men are
often tempted, I wish to advise them that it is a school, in which
profanity, coarseness, intemperance, and vice, are effectually taught.
It is a seminary where almost every thief, robber, counterfeiter, and
murderer, takes his first and last lesson. A man who loves a bar-
room where liquors are sold, has reason to tremble; a young man
who loves bar-room company, has already entered within the very
gate that leads down to ruin. That I have escaped such ruin myself,
is attributable to the kindness of Providence, rather than to any
resistance of evil which originated in my own breast. If Heaven had
deserted me, I had been lost forever.
It was one night after we had been drinking at the tavern, that my
companions and myself issued forth, bent on what was called a
spree. Our first exploit was to call up the doctor of the village, and
ask him to hasten to Miss Sally St. John, who has been noticed
before in these memoirs, insinuating that she was desperately ill.
Our next adventure was to catch the parson’s horse in the pasture,
and tie him to the whipping-post, which stood on the green before
the meeting-house. We then proceeded to a watermelon patch, and,
prowling about among the vines, selected the largest and finest, and
ripping them open, strewed the contents over the ground. We then
went to a garden belonging to a rich old farmer, who was celebrated
for producing very fine pears. The window of the proprietor looked
out into the garden, and as he had the reputation of exercising a
vigilant watch over his fruit, we felt the necessity of caution. But we
were too much elated by our liquor and success in sport, to be very
circumspect. We got over the tall picket fence, and two or three of us
ascended one of the trees. We had begun already to pluck the fruit,
when the window of the old farmer slid silently upward, and a
grizzled head was thrust out. It was soon withdrawn, but in a few
moments the barrel of a long gun was pushed forth, and a second
after it discharged its contents, with a sound which, at that silent
hour, seemed like the voice of thunder.
I was on the tree, with my back to the marksman, and presented a
fair target to his aim. At the very instant of the discharge, I felt a
tingling in my flesh; immediately after a dizziness came over my
sight, and I fell to the ground. I was completely stunned, but my
companions seized me and hurried me away. Clambering over stone
walls, and pushing through a nursery of young trees, they secured
their retreat. At a safe distance the party paused, and after a little
space I recovered my senses. I found myself in great pain, however,
and after a little examination it appeared that my left arm was
broken. As carefully as possible I was now taken toward my home. It
was about midnight when we reached it, and my uncle, being
informed that I was hurt, attempted to come to me. But he had been
in bed but a short time, and according to his wont, about this period,
he had taken a “night-cap,” as he called it, and was utterly incapable
of walking across the floor. Some of the people, however, were got
up, and one went for the physician. The answer returned was, that
some madcaps had been there and played off a hoax upon the
doctor, and this application was no doubt intended as another, and
he would not come. I therefore lay till morning in great distress, and
when at last the doctor came, he found that not only my arm was
broken, but that my back was wounded, as if I had been shot with
bullets of salt! Several small pieces of salt were actually found
imbedded in my skin!
I was hardly in a state to give explanations; in fact, my reason
already began to waver. Strange visions soon flitted before my eyes:
an old grizzled pate seemed bobbing out of a window, and making
faces at me; then the head seemed a watermelon with green eyes;
and then it turned into a bell-muzzled fowling-piece, and while I was
trying to look down its throat, it exploded and scattered my brains to
the four winds! Here my vision ended, and with it all remembrance. I
fell into a settled fever, and did not recover my senses for two weeks.
When my consciousness returned, I found myself attended by a man
of the village, named Raymond, a brother of the minister, and whom
I had long known. He was sitting by my bedside, with a book in his
hand; but as I opened my eyes, I noticed that, while he seemed to be
reading, his eyes were fixed on me with an anxious interest. In a
moment after he spoke. “Are you better, Robert?” said he, in a tone
of tenderness. I attempted to reply, but my tongue refused to move.
Raymond saw my difficulty, and coming to the bedside, told me to
remain quiet. “You have been ill,” said he, “very ill, but you are better.
Your life depends upon your being kept perfectly quiet.”
Thus admonished, I closed my eyes, and soon fell asleep. The
next day I was much better, and entered into some conversation with
Raymond, who I then found had been my regular attendant. The
physician soon after came, and pronounced me out of danger. “You
are better, my young friend,” said he; “I think you are safe; but this
getting salted down like a herring, and tumbling off of pear trees at
midnight, is an awkward business, and cannot be often repeated
with impunity.” This latter remark being uttered with a significant
smile, recalled to my mind the occasion of my sickness, and a
sudden blush of shame covered my face. Raymond noticed my
confusion, and by some remark immediately diverted my attention to
another topic.
In a few days I was able to sit up in my bed, and was nearly free
from pain. My arm, however, was still useless, and I was in fact very
feeble. I could talk with Raymond, however, and as his conversation
was always engaging, the time did not pass heavily. Raymond was a
man of extensive reading, and great knowledge of the world, but,
owing to excessive sensitiveness, he had settled into a state of
almost complete imbecility. He thought and spoke like a philosopher,
yet in the active business of life, in which he had been once
engaged, he had entirely failed. He was indeed regarded in the
village as little better than insane or silly. He had no regular
employment, and spent his time almost wholly in reading—his
brother, the minister, having a good library. As he was very kind-
hearted, however, and possessed a good deal of medical
knowledge, he was often employed in attending upon sick persons,
and for his services he would never receive any other compensation
than his own gratification, in the consciousness of doing good, might
afford.
It was a mercy to me that I fell into the hands of poor Raymond,
for my mind and heart were softened by my sickness, and by the
humiliation I felt at having been detected in a disgraceful act, and so
signally punished. His counsel, therefore, which was full of wisdom,
and which he imparted in a way, at once to instruct and amuse, sunk
into my mind like the seed sown in spring time, and upon a prepared
soil; and I have reason to believe that I may attribute not only the
recovery of my body from disease, but the correction of some of the
vices of my mind, to his conversations at my sick bedside. I believe I
cannot do my readers a better service than to transcribe some of
these conversations, as nearly as my memory will restore them, and
this I shall do in a subsequent chapter.
Toucan
Is the name of the bird whose picture is here given. I beg my

reader not to laugh at his enormous bill, for it is such as nature has
given him, and he is no more to blame for it than a person with a
long nose, is to blame for having such a one. Bonaparte said that a
man with a long nose almost invariably possessed good sense; and
this holds true in respect to the toucan; for I assure you he is a very
clever fellow in his way. I will tell you all about him and his family.
The toucans are natives of South America, and are very abundant
in the forests of Brazil. They only dwell in the warm parts of the
country, and they select those portions which are the richest in their
productions. It is among spicy groves, and where fruits and flowers
are to be found at all seasons of the year, that the toucan family
have chosen to make their home. Surely this seems a mark of their
sagacity.
The toucan is about eighteen inches in length, and its general
color is black, though it is marked with crimson and yellow, and is a
very stylish bird. The bill is almost as long as the body, but it is less
bony than the bills of other birds; it is, in fact, a great part of it but a
thin paper-like substance. Those portions which need to be strong
are not solid bone, but consist of two thin laminæ, sustained by
bones within, and crossing each other like the timbers which support
the sides and roof of a house.
I have intimated that the toucans are pretty sensible birds, and I
shall now attempt to prove it. As their legs are very short and far
apart, they cannot walk very well on the ground, so they spend a
great portion of their time upon the wing, or upon the trees. They
have strong, sharp claws, well fitted for climbing; so they are very
much addicted to hopping about among the branches of trees, and
they may be often seen, like woodpeckers, running up and down the
trunks. It is for this climbing propensity that they have got the name
of Zygodactilic birds,—a long word, which no doubt signifies a great
deal.
Another proof of the good sense of the toucan is furnished by his
always sitting and flying with his head to the wind when it blows hard
—for the reason, that, if he presented the broadside of his proboscis
to the gale, it would bother him to keep himself from being
completely blown away. Beside this proof of his sagacity, I may add,
that the toucan holds the monkeys, who are very abundant and
troublesome in his country, in great detestation; and well he may, for
the monkey is fond of birds’ eggs, and is a great robber of birds’
nests. Now the toucan likes eggs himself, and the plundering
monkey often deprives the toucan of his breakfast, by getting at the
nest first. It is not wonderful that squabbles often ensue between
these rival thieves—for two of a trade can never agree, you know. Of
course, the robbers care as little for the poor bird that is robbed, as
lawyers for their clients—but they think a great deal of themselves,
and when interest is touched, they resent it manfully. There is
something in a monkey and a toucan over a bird’s nest that seems
like two lawyers over a case. Their mutual object is to eat up the
eggs, but it makes a mighty difference which gets them. If the
monkey gets the case, toucan gives him a tweak with his enormous
bill, which gripes like a pair of tongs. If toucan gets the case, monkey
slaps him across his beak with the palm of his hand, and often with
such force as to make toucan scream outright. It must be admitted
that if toucan has a large bill to bite with, he also presents an ample
mark for the revenge of monkey. Whether these squabbles show the
good sense of toucan, I will not decide, but he can plead the
example of one of the learned professions, that of the law, which
ranks among the first in society, and exerts more influence over
mankind than all others put together.
Another evidence of toucan’s good sense is this,—that he eats
everything he likes, if it suits his constitution. There is a delicious
little fruit in his native clime, called toucan-berry, which is good for his
health, so he feasts upon it when he can get it. He also eats eggs, as
I have said; and, in short, he diversifies, and amplifies his pleasures,
like civilized men, by fruit, flesh, fowl, or vegetable, if it agrees with
him.
I do not know that I need to say more at present, than that toucan
does not choose to take the trouble of making nests of stems and
twigs, like some other birds, but selects his dwelling in the holes of
trees, so that he may have a roof to shelter him from the storm—a
preference which again marks his civilization.
THE NEWFOUNDLAND DOG.
The Newfoundland Dog.
Of all animals, the dog is most attached to man. His affection is

not general, but particular. He does not love all mankind, as a matter
of course, for in his natural state he is a wild and savage creature. In
Asia, dogs are often outcasts, prowling around cities, and feeding
upon offal and dead carcasses. They seem to be, if uncivilized,
cousins to the wolf, and near relatives to the hyena. It is in Asia,
where the dog is a persecuted, and therefore a skulking kind of
animal, that he is the emblem of meanness and cowardice. There,
where the people worship power and seem to think little of justice,
the lion, a sly, prowling, thieving creature, is the common emblem of
courage and greatness.
But here, where the dog is cherished and taken to a home, he
seems to have a new character and a redeemed nature. He fixes his
heart upon some one, and is ready to run, jump, bark, bite, dig, work
or play, to give pleasure to him. He seems to live for his master—his
master is his deity. He will obey and defend him while living—he will
lie down and die by his master’s grave. It is related of Bonaparte,
that one night, after a fight, he was walking by the moonlight over the
field of battle, when suddenly a dog sprung out from the cloak
beneath which his dead master lay, and then ran howling back to the
body, seeming at the same time to ask help for his poor friend, and
to seek revenge. Bonaparte was much affected by the scene, and
said that few events of his life excited a deeper feeling in his breast
than this.
There are at least thirty different kinds of dogs,—some large,
some small, some fierce, some gentle, some slender and graceful,
some sturdily made and very powerful. There is the lap-dog, with a
soft, lustrous eye and silken skin, fit to be the pet of a fine lady—and
there is the fierce bull-dog, that will seize a bull by the nose and pin
him to the ground. There is the greyhound, that is so swift as to
outstrip the deer, and the patient foxhound, that follows reynard with
a keen scent, till at last his fleetness and his tricks can avail him
nothing, and he surrenders to his fate.
But amid all this variety, the Newfoundland dog is the best fellow.
He is, in the first place, the most intelligent, and in the next, he is the
most devoted, attached, and faithful. When the people came from
Europe to America, they found this fine breed of dogs with the
Indians of Newfoundland and the vicinity. They are large, shaggy,
webfooted, and almost as fond of the water as the land. They
possess great strength, and have a countenance that seems to
beam with reason and affection. I give you the portrait of one of
these creatures, to prove what I say. There are many pleasant tales
of this creature, well authenticated, of which I shall now tell you a
few.
One day, as a girl was amusing herself with an infant, at Aston’s
Quay, near Carlisle bridge, Dublin, and was sportively toying with the
child, it made a sudden spring from her arms, and in an instant fell
into the Liffey. The screaming nurse and anxious spectators saw the
water close over the child, and conceived that he had sunk to rise no
more. A Newfoundland dog, which had been accidentally passing
with his master, sprang forward to the wall, and gazed wistfully at the
ripple in the water, made by the child’s descent. At the same instant
the child reappeared on the surface of the current, and the dog
sprang forward to the edge of the water.
Whilst the animal was descending, the child again sunk, and the
faithful creature was seen anxiously swimming round and round the
spot where it had disappeared. Once more the child rose to the
surface; the dog seized him, and with a firm but gentle pressure bore
him to land without injury. Meanwhile a gentleman arrived, who, on
inquiry into the circumstances of the transaction, exhibited strong
marks of sensibility and feeling towards the child, and of admiration
for the dog that had rescued him from death.
The person who had removed the babe from the dog turned to
show the infant to this gentleman, when it presented to his view the
well-known features of his own son! A mixed sensation of terror, joy,

Dynamic Logic New Trends and

Uploaded by

Copyright:

Available Formats

Dynamic Logic New Trends and

Uploaded by

Document Information

Original Title

Copyright

Available Formats

Share this document

Share or Embed Document

Sharing Options

Did you find this document useful?

Is this content inappropriate?

Copyright:

Available Formats

Dynamic Logic New Trends and

Uploaded by

Copyright:

Available Formats

Full download test bank at ebook textbookfull.

Dynamic Logic New Trends and

Logic, Language, Information, and Computation: 24th

Mobility Analytics for Spatio Temporal and Social Data

Analytical and Computational Methods in Probability

Provable Security: 11th International Conference,

Interactive Storytelling 10th International Conference

ICIBSoS 2017 : Proceedings of the 6th International

Exploring Services Science 8th International Conference

Cyberspace Safety and Security 9th International

ISSN 0302-9743 ISSN 1611-3349 (electronic)

Library of Congress Control Number: 2017962907

LNCS Sublibrary: SL1 – Theoretical Computer Science and General Issues

© Springer International Publishing AG 2018

Printed on acid-free paper

This Springer imprint is published by Springer Nature

pleasure of hosting a special talk entitled “Dynamic Logic, a Personal Perspective,” by

September 2017 Mario Benevides

Undecidability of Relation-Changing Modal Logics. . . . . . . . . . . . . . . . . . . 1

Axiomatization and Computability of a Variant of Iteration-Free

A Dynamic Logic for Learning Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

Layered Logics, Coalgebraically . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

A Dynamic Informational-Epistemic Logic . . . . . . . . . . . . . . . . . . . . . . . . . 64

Dynamic Epistemic Logics of Introspection . . . . . . . . . . . . . . . . . . . . . . . . 82

Logics for Actor Networks: A Case Study in Constrained Hybridization . . . . 98

Parity Games and Automata for Game Logic . . . . . . . . . . . . . . . . . . . . . . . 115

Model Checking Against Arbitrary Public Announcement Logic:

Dynamic Logic: A Personal Perspective . . . . . . . . . . . . . . . . . . . . . . . . . . . 153

The Creation and Change of Social Networks: A Logical Study

Dynamic Preference Logic as a Logic of Belief Change. . . . . . . . . . . . . . . . 185

Author Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201

Carlos Areces1,2 , Raul Fervari1,2(B) , Guillaume Hoﬀmann1,2 ,

Abstract. Relation-changing modal logics are extensions of the basic

Keywords: Modal logics · Dynamic logics · Satisﬁability

logic ML( r , k ) and a sketch of the proof of its undecidability. We dedicate

2 Relation-Changing Modal Logics

Definition 1 (Syntax). Let PROP be a countable, inﬁnite set of propositional

FORM ::= p | ¬ϕ | ϕ ∧ ψ | ♦ϕ | ϕ,

Semantically, formulas are evaluated in standard relational models, and the

Definition 2 (Models and model updates). A model M is a triple M =

(swapping) M∗S = W, RS∗ , V , with RS∗ = (R\S −1 )∪S, S ⊆ R−1 .

Definition 3 (Semantics). Given a pointed model M, w and a formula ϕ, we

We say ϕ is satisﬁable if for some pointed model M, w, we have M, w |= ϕ.

3 Undecidability of Monomodal Memory Logic

where p ∈ PROP and ϕ, ψ ∈ FORM. Other operators are deﬁned as usual.

W, R, V, S, w |= r ϕ iﬀ W, R, V, S ∪ {w}, w |= ϕ

Multimodal memory logic is shown to be undecidable in [7]. We strengthen

Theorem 1. The satisﬁability problem of ML( r , k ) is undecidable.

Proof. The problem of concept consistency in the description logic ALCself is

We previously suggested that relation-changing operators could, each one in

Definition 6 (PNF). An ML( r , k )-formula is in proper normal form (PNF)

Finally, we deﬁne the notion of modal depth of an ML( r , k )-formula.

Definition 7. Given ϕ in ML( r , k ), we deﬁne the modal depth of ϕ (notation

In the next section we prove that the satisﬁability problem of relation-

4 Undecidability of Relation-Changing Logics

Theorem 2. The satisﬁability problem of ML() is undecidable, for ∈ {sb,

The main idea of these translations is to simulate the behavior of ML( r , k )

Definition 8. Deﬁne τsb (ϕ) = Structsb ∧ Trsb (ϕ), where:

Structsb = s ∧ ¬s (1)

(swapping) M∗S = W, RS∗ , V , with RS∗ = (R\S −1 )∪S, S ⊆ R−1 .

W, R, V, S, w |= r ϕ iﬀ W, R, V, S ∪ {w}, w |= ϕ

Theorem 2. The satisﬁability problem of ML() is undecidable, for ∈ {sb,

Definition 8. Deﬁne τsb (ϕ) = Structsb ∧ Trsb (ϕ), where:

Structsb = s ∧ ¬s (1)

Trsb (ϕ) = ♦(ϕ) , with:

(p) = p f or p ∈ PROP appearing in ϕ

Proposition 1. If W, R, V , w |= Structsb , then for every state v ∈ W \ {w}

Proof. (⇐) Suppose W, R, V , s |= τsb (ϕ). Let W = W \V (s), R = R ∩ (W ×

construction, W , R , V , s |= Structsb , so Proposition 1 holds. We prove that

Definition 9. Deﬁne τgsb (ϕ) = Structgsb (ϕ) ∧ Trgsb (ϕ), where:

Trgsb (p) = p f or p ∈ PROP appearing in ϕ

Proposition 3. If W, R, V , w |= ♦s ∧ gsb¬♦s, then w has one and only one

Proof. (⇐) Suppose W, R, V , w |= τgsb (ϕ). Let W = W \V (s), R = R∩(W ×

PROP appearing in ϕ. It is easy to check that W , R , V , w |= Structgsb (ϕ),

Lemma 3. Let ϕ = s ∧ ⊥ ∧ [br](s→[br]¬s). If M, w |= ϕ, then w is the only

Definition 10. Deﬁne τbr (ϕ) = Structbr ∧ Trbr (ϕ), where:

Structbr = s ∧ ⊥ ∧ [br](s→[br]¬s) (1)

Trbr (ϕ) = br(¬s ∧ t ∧ br(¬s ∧ ¬t ∧ (ϕ) )), with:

(p) = p f or p ∈ PROP appearing in ϕ

Proof. (⇐) Suppose W, R, V , s |= τbr (ϕ). Deﬁne M = W , R , V , ∅ with

p ∈ PROP appearing in ϕ. We can easily check that W , R, V , s |= Structbr ,

Trgbr (p) = p f or p ∈ PROP appearing in ϕ

U niq = ♦(s ∧ ⊥) ∧ [sw](s → ¬♦s)

Trsw (ϕ) = ♦(ϕ) , with:

(p) = p f or p ∈ PROP appearing in ϕ

Proposition 5. Let W, R, V , s |= Structsw , W = W \ V (s) and S ⊆ W .

Then, by deﬁnition of RS and inductive hypothesis we get W, (RS )∗v v , V , v |=

Trgsw (p) = p f or p ∈ PROP appearing in ϕ

Proposition 6. Let W, R, V , w |= ¬♦s ∧ gsw♦s. Then, by the semantics of

Example 2. If α = aΔb, f (α) = (a; ?)Δ(b; ?).