计算机科学中的逻辑

We present process-algebraic models of multi-writer multi-reader safe, regular and atomic registers. We establish the relationship between our models and alternative versions presented in the literature. We use our models to formally…

In epistemic logic, a way to deal with knowledge-wh is to interpret them as a kind of mention-some knowledge (MS-knowledge). But philosophers and linguists have challenged both the sufficiency and necessity of such an account: some argue…

This paper presents a logic-based framework to analyze responsibility, which I refer to as intentional epistemic act-utilitarian stit theory (IEAUST). To be precise, IEAUST is used to model and syntactically characterize various modes of…

In this paper we formalise three types of cognitive bias within the framework of belief revision: confirmation bias, framing bias, and anchoring bias. We interpret them generally, as restrictions on the process of iterated revision, and we…

Binary decision diagrams (BDDs) are widely used to mitigate the state-explosion problem in model checking. A variation of BDDs are Zero-suppressed Decision Diagrams (ZDDs) which omit variables that must be false, instead of omitting…

The logic of goal-directed knowing-how extends the standard epistemic logic with an operator of knowing-how. The knowing-how operator is interpreted as that there exists a strategy such that the agent knows that the strategy can make sure…

We observe some puzzling linguistic data concerning ordinary knowledge ascriptions that embed an epistemic (im)possibility claim. We conclude that it is untenable to jointly endorse both classical logic and a pair of intuitively attractive…

Two level credibility-limited revision is a non-prioritized revision operation. When revising by a two level credibility-limited revision, two levels of credibility and one level of incredibility are considered. When revising by a sentence…

Arbitrary Public Announcement Logic with Common Knowledge (APALC) is an extension of Public Announcement Logic with common knowledge modality and quantifiers over announcements. We show that the satisfiability problem of APALC on S5-models,…

Any kind of dynamics in dynamic epistemic logic can be represented as an action model. Right? Wrong! In this contribution we prove that the update expressivity of communication patterns is incomparable to that of action models. Action…

Epistemic logics of intensional groups lift the assumption that membership in a group of agents is common knowledge. Instead of being represented directly as a set of agents, intensional groups are represented by a property that may change…

This work builds upon a well-established research tradition on modal logics of awareness. One of its aims is to export tools and techniques to other areas within modal logic. To this end, we illustrate a number of significant bridges with…

Awareness structures by Fagin and Halpern (1988) (FH) feature a syntactic awareness correspondence and accessibility relations modeling implicit knowledge. They are a flexible model of unawareness, and best interpreted from a outside…

Correspondence theory allows us to create sound and complete axiomatizations for modal logic on frames with certain properties. For example, if we restrict ourselves to transitive frames we should add the axiom $\square \phi \rightarrow…

In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. The behavior of every process is given by a pushdown automaton. We consider infinite behaviors of such systems under strong…

Linearizability is a standard correctness criterion for concurrent algorithms, typically proved by establishing the algorithms' linearization points. However, relying on linearization points leads to proofs that are…

We consider networks of processes that all execute the same finite-state protocol and communicate via a rendez-vous mechanism. When a process requests a rendez-vous, another process can respond to it and they both change their control…

Probabilistic hyperproperties specify quantitative relations between the probabilities of reaching different target sets of states from different initial sets of states. This class of behavioral properties is suitable for capturing…

We carry on the study of the synthesis problem on data words for fragments of first order logic, and delineate precisely the border between decidability and undecidability.

In categorical realizability, it is common to construct categories of assemblies and categories of modest sets from applicative structures. These categories have structures corresponding to the structures of applicative structures. In the…