Search

Various extensions of public announcement logic have been proposed with quantification over announcements. The best-known extension is called arbitrary public announcement logic, APAL. It contains a primitive language construct Box phi intuitively expressing that "after every public announcement of a formula, formula phi is true". The logic APAL is undecidable and it has an infinitary axiomatization. Now consider restricting the APAL quantification to public announcements of Boolean formulas only, such that Box phi intuitively expresses that "after every public announcement of a Boolean formula, formula phi is true". This logic can therefore called Boolean arbitrary public announcement logic, BAPAL. The logic BAPAL is the subject of this work. Unlike APAL it has a finitary axiomatization. Also, BAPAL is not at least as expressive as APAL. A further claim that BAPAL is decidable is deferred to a companion paper.

Dynamic epistemic logics consider formal representations of agents' knowledge, and how the knowledge of agents changes in response to informative events, such as public announcements. Quantifying over informative events allows us to ask whether it is possible to achieve some state of knowledge, and has important applications in synthesising secure communication protocols. However, quantifying over quite simple informative events, public announcements, is not computable: such an arbitrary public announcement logic, APAL, has an undecidable satisfiability problem. Here we consider even simpler informative events called Boolean announcements, where announcements are restricted to be a Boolean combination of atomic propositions. The logic is called Boolean arbitrary public announcement logic, BAPAL. A companion paper provides a complete finitary axiomatization, and related expressivity results, for BAPAL. In this work the satisfiability problem for BAPAL is shown to decidable, and also that BAPAL does not have the finite model property.

Description logics are a powerful tool for describing ontological knowledge bases. That is, they give a factual account of the world in terms of individuals, concepts and relations. In the presence of uncertainty, such factual accounts are not feasible, and a subjective or epistemic approach is required. Aleatoric description logic models uncertainty in the world as aleatoric events, by the roll of the dice, where an agent has subjective beliefs about the bias of these dice. This provides a subjective Bayesian description logic, where propositions and relations are assigned probabilities according to what a rational agent would bet, given a configuration of possible individuals and dice. Aleatoric description logic is shown to generalise the description logic ALC, and can be seen to describe a probability space of interpretations of a restriction of ALC where all roles are functions. Several computational problems are considered and model-checking and consistency checking algorithms are presented. Finally, aleatoric description logic is shown to be able to model learning, where agents are able to condition their beliefs on the bias of dice according to observations., Short version submitted to DL2021

We consider multi-agent systems where agents actions and beliefs are determined aleatorically, or "by the throw of dice". This system consists of possible worlds that assign distributions to independent random variables, and agents who assign probabilities to these possible worlds. We present a novel syntax and semantics for such system, and show that they generalise Modal Logic. We also give a sound and complete calculus for reasoning in the base semantics, and a sound calculus for the full modal semantics, that we conjecture to be complete. Finally we discuss some application to reasoning about game playing agents., Comment: Long version of paper accepted to appear at the 2019 Indian Conference on Logic and Applictaions

Automata expressiveness is an essential feature in understanding which of the formalisms available should be chosen for modelling a particular problem. Probabilistic and stochastic automata are suitable for modelling systems exhibiting probabilistic behavior and their expressiveness has been studied relative to non-probabilistic transition systems and Markov chains. In this paper, we consider previous formalisms of Timed, Probabilistic and Stochastic Timed Automata, we present our new model of Timed Automata with Polynomial Delay, we introduce a measure of expressiveness for automata we call trace expressiveness and we characterize the expressiveness of these models relative to each other under this new measure., possibly incorrect, or unsubstantiated results and claims

We consider previous models of Timed, Probabilistic and Stochastic Timed Automata, we introduce our model of Timed Automata with Polynomial Delay and we characterize the expressiveness of these models relative to each other., Comment: possibly incorrect, or unsubstantiated results and claims

We compare different epistemic notions in the presence of awareness of propositional variables: the logics of implicit knowledge (in which explicit knowledge is definable), explicit knowledge, and speculative knowledge. Different notions of bisimulation are suitable for these logics. We provide correspondence between bisimulation and modal equivalence on image-finite models for these logics. The logic of speculative knowledge is equally expressive as the logic of explicit knowledge, and the logic of implicit knowledge is more expressive than both. We also provide axiomatizations for the three logics -- only the one for speculative knowledge is novel. Then we move to the study of dynamics by recalling action models incorporating awareness. We show that any conceivable change of knowledge or awareness can be modelled in this setting, we give a complete axiomatization for the dynamic logic of implicit knowledge. The dynamic versions of all three logics are, surprising, equally expressive., Comment: 10 pages, Contributed talk at TARK 2013 (arXiv:1310.6382) http://www.tark.org

This paper proposes a new logic RoCTL* to model robustness in concurrent systems. RoCTL* extends CTL* with the addition of Obligatory and Robustly operators, which quantify over failure-free paths and paths with one more failure respectively. We present a number of examples of problems to which RoCTL* can be applied. The core result of this paper is to show that RoCTL* is expressively equivalent to CTL* but is non-elementarily more succinct. We present a translation from RoCTL* into CTL* that preserves truth but may result in non-elementary growth in the length of the translated formula as each nested Robustly operator may result in an extra exponential blowup. However, we show that this translation is optimal in the sense that any equivalence preserving translation will require an extra exponential growth per nested Robustly. We also compare RoCTL* to Quantified CTL* (QCTL*) and hybrid logics.