计算机科学中的逻辑

Colored Petri nets offer a compact and user friendly representation of the traditional P/T nets and colored nets with finite color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in…

We propose an interpretation of multiparty sessions with asynchronous communication as Flow Event Structures. We introduce a new notion of global type for asynchronous multiparty sessions, ensuring the expected properties for sessions,…

We contemplate the notion of ambiguity in mathematical discourse. We consider a general method of resolving ambiguity and semantic options for sustaining a resolution. The general discussion is applied to the case of `fraction' which is…

Sabotage games are played on a dynamic graph, in which one agent, called a runner, attempts to reach a goal state, while being obstructed by a demon who at each round removes an edge from the graph. Sabotage modal logic was proposed to…

Nontrivial combinatory algebras with S and K must be infinite. Associativity is incompatible with combining a classifier and a retraction pair in a finite extensional magma. These obstructions exclude several standard settings from the…

Awareness-Based Indistinguishability Logic (henceforth, AIL) is an extension of Epistemic Logic by introducing the notion of awareness, distinguishing explicit knowledge from implicit knowledge. In this framework, each of these notions is…

The logic of awareness, first proposed by Fagin and Halpern, addressed the problem of logical omniscience by introducing the notion of awareness and distinguishing explicit knowledge from implicit knowledge. In their framework, explicit…

We extend the complete ordered set Dana Scott's $D_\infty$ to a complete weakly ordered Kan complex $K_\infty$, with properties that guarantee the non-equivalence of the interpretation of some higher conversions of $\beta\eta$-conversions…

Two major milestones on the road to the full complexity dichotomy for finite-domain constraint satisfaction problems were Bulatov's proof of the dichotomy for conservative templates, and the structural dichotomy for smooth digraphs of…

Reasoning about consistency models for replicated data systems is a challenging task that requires a deep understanding of both the consistency models themselves and a large part of human inputs in mechanized verification approaches. In…

These proceedings contain the papers that were presented at the 7th Workshop on Models for Formal Analysis of Real Systems (MARS 2026), which took place on 12 April 2026 in Turin, Italy, as a satellite event of the 29th International Joint…

Assume-guarantee reasoning is a technique for compositional model checking in which system specifications are checked under certain assumptions on system parameters or inputs, and provide guarantees on observations of system state. We…

We develop a logic of secrecy on simplicial models for multi-agent systems. Standard simplicial models provide a geometric semantics for knowledge by representing global states as facets of a chromatic simplicial complex and agents' local…

We introduce and study UCPDL+, a family of expressive logics rooted in Propositional Dynamic Logic (PDL) with converse (CPDL) and universal modality (UCPDL). In terms of expressive power, UCPDL+ strictly contains PDL extended with…

Boolean networks are extensively applied as models of complex dynamical systems, aiming at capturing essential features related to causality and synchronicity of the state changes of components along time. Dynamics of Boolean networks…

The rapid evolution of autonomous, agentic artificial intelligence within financial services has introduced an existential architectural crisis: large language models (LLMs) are probabilistic, non-deterministic systems operating in domains…

We present a framework for compositional program verification based on polynomial functors in dependent type theory. In this framework, polynomial functors serve as program interfaces, Kleisli morphisms for the free monad monad serve as…

We verify the correctness of a variety of mutual exclusion algorithms through model checking. We look at algorithms where communication is via shared read/write registers, where those registers can be atomic or non-atomic. For the…

We present PBLean, a method for importing VeriPB pseudo-Boolean (PB) proof certificates into Lean 4. Key to our approach is reflection: a Boolean checker function whose soundness is fully proved in Lean and executed as compiled native code.…

In this paper, we define the notion of {\em probabilistic $\omega$-pushdown automaton} and study its model-checking problem against the logic of $\omega$-probabilistic computational tree logic ($\omega$-PCTL) and its bounded version from a…