A framework for computing upper bounds in passive learning settings
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.
On Temporal References via Definite Descriptions in First-Order Monadic Logic of Order
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.
Alternating-Time Temporal Logic with Default Actions
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.
Engineering and Evaluating Multi-objective Pseudo-boolean Optimizers
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.
Unsupervised Automata Learning via Discrete Optimization
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.
Finding short tree-like unit refutations in UTVPI Constraint Systems
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.
Exposure and Hiding: Approaching the Objective Probability and Hiding the Secret in Zero-Knowledge Proof
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.