ABSTRACT. Temporal reference, understood as the capability of referring to particular points of time, is an essential aspect of temporal reasoning. In this paper we model it with the definite description (iota) operator added to first-order monadic logic of order—a standard formalism for reasoning about time. This allows us to express temporal reference directly and with dedicated tools, which is of particular importance from the point of view of proof systems for automated reasoning. We construct a sound and complete tableau system, as well as provide complexity results for the satisfiability problem of the obtained logic.

ABSTRACT. The task of inferring logical formulas from examples has garnered significant attention as a means to assist engineers in creating formal specifications used in the design, synthesis, and verification of computing systems. Among various approaches, enumeration algorithms have emerged as some of the most effective techniques for this task. These algorithms employ advanced strategies to systematically enumerate candidate formulas while minimizing redundancies by avoiding the generation of syntactically different but semantically equivalent formulas. However, a notable drawback is that these algorithms typically do not provide guarantees of termination.

This paper develops an abstract framework to bound the size of possible solutions for a logic inference task, thereby providing a termination guarantee for enumeration algorithms through the introduction of a sufficient stopping criterion. The proposed framework is designed with flexibility in mind and is applicable to a broad spectrum of practically relevant logical formalisms, including Modal Logic, Linear Temporal Logic, Computation Tree Logic, Alternating-time Temporal Logic, Probabilistic Computation Tree Logic and even selected inference task for automata. In addition, our approach enabled us to develop a meta algorithm that enumerates over the semantics of formulas rather than their syntactic representations, offering new possibilities for reducing redundancy.

ABSTRACT. We introduce an extension of Alternating-Time Temporal Logic (ATL) that incorporates default actions to model communication failures in multi-agent systems. Our framework, ATL-kD, allows for limited number of communication failures during which agents’ intended strategies may not be delivered. In the event of such a communication failure, a predefined default action is played. We analyse the computational complexity of model checking in this setting, showing NP-hardness and coNP-hardness in general, but polynomial-time solvability when default actions are restricted to a fixed subset of agents.

We also examine a variant with default preferences, which better handles cases where the default action mights be unavailable in some states due to protocol constraints. Additionally, we introduce default action updates, allowing the default action to be revised during system execution. Together, these results provide a formal foundation for robust verification under unreliable communication.

ABSTRACT. Various real-world settings give rise to combinatorial optimization problems with multiple conflicting objectives, motivating the development of practical approaches to the challenging task of finding Pareto-optimal solutions to declarative models of multi-objective problems. In this work we focus on multi-objective optimization over pseudo-Boolean constraints as an important class of integer linear constraints. We provide a first-of-kind cross-community evaluation of a selection of recently-proposed approaches applicable to MO-PBO, including first implementations of native MO-PBO algorithms we provide as well as approaches based on integer linear programming techniques and a translation-based approach to MO-MaxSAT, providing insights into the current state-of-the-art approaches to MO-PBO. In terms of algorithmic advances, we engineer MO-PBO solvers by lifting multi-objective approaches recently developed for multi-objective optimization under propositional constraints (i.e., MO-MaxSAT) to the realm of MO-PBO by harnessing recent advances in decision procedures for pseudo-Boolean constraints. Extending on recent work on certified MO-MaxSAT solving, we also realize certified multi-objective pseudo-Boolean optimization by implementing proof logging for both our native MO-PBO approach and the translation-based MO-MaxSAT approach.

ABSTRACT. In the last decades, automata learning has proven to be a successful tool in many application domains such as robotics and automatic verification. Typically, automata learning techniques operate in a supervised learning setting (active or passive) where they learn a finite state machine in settings where addi- tional information, such as labeled system executions, is available. However, other settings, such as learning from unlabeled data - an important aspect in machine learning - remain unexplored. To overcome this limitation, we propose a frame- work for learning a deterministic finite automaton (DFA) from a given multi-set of unlabeled words. We show that this problem is computationally hard and develop three learning algorithms based on constraint optimization. Moreover, we intro- duce novel regularization schemes for our optimization problems that improve the overall interpretability of our DFAs. Using a prototype implementation, we demonstrate practical feasibility in the context of unsupervised anomaly detection.

ABSTRACT. In this paper, we investigate unit refutability in Unit Two Variable Per Inequality (UTVPI) Constraint Systems (UCSs). A Unit Two Variable Per Inequality (UTVPI) constraint is a linear relationship of the form: $\pm x_{i}\pm x_{j} \le b_{ij}$, where $b_{ij} \in \mathbb{Z}$. A UCS is a conjunction of such constraints. If it is required that the two variables in a UTVPI constraint have opposite signs, then the constraint is called a difference constraint and a conjunction of such constraints is called a difference constraint system (DCS). When a decision procedure deems a UCS is infeasible, it is important to provide a certificate which attests to the infeasibility of the UCS. Such a certificate is called a negative certificate. Refutations (under an appropriate refutation system) form an important subclass of negative certificates. All problems in the complexity class {\bf P} have succinct negative certificates. We focus on a subclass of refutations called Unit Refutations (UR). The UR refutation system is {\bf incomplete}, in that unsatisfiable UCSs may not have unit refutations. However, they are useful from the perspective of identifying variable domains responsible for system inconsistency. Previous work has examined dag-like unit refutations of UCSs \cite{walcom25}. In this paper, we examine tree-like unit refutations of UCSs.

ABSTRACT. Zero-knowledge proofs (ZKPs) enable a prover to convince a verifier that she is holding a secret without revealing any information on the secret. This paper formalizes a widely-used ZKP protocol, i.e.,Schnorr protocol, using Probabilistic Hoare Logic (PHL) and Product Probabilistic Relational Hoare Logic (xPRHL). The deterministic states are defined based on the set-extension style, which captures the information change of the participants in the protocol. In contrast to the classical PHL, we set the probabilistic states as the probability distributions over flexible spaces of deterministic states. Commands can bring about the transition between the novel probabilistic states. Precisely, PHL captures the probability that a prover always passes the challenges proposed by the verifier asymptotically approaches 1 if the prover indeed holds the secret. Moreover, we investigate the Schnorr protocol based on a generalized setting, where the initial probabilistic state assigns the probability of holding the secret p (rather than 1 or 0) and that of not holding 1-p (rather than 0 or 1, respectively). Based on this characterization, the ZKP protocol can be seen as a method to `expose' the probability p of a prover holding a secret when p is initially not known by anyone. xPRHL constructs a coupled product program to prove computational indistinguishability between the real protocol and a simulator, demonstrating the zero-knowledge property. Our work provides a novel formal framework for analyzing and understanding ZKPs and highlights the advantages of probabilistic reasoning in cryptographic verification.