1

Incremental NFA Minimization

Finite state automata are fundamental objects in Theoretical Computer Science and find their application in Text Processing, Compilers Design, Artificial Intelligence and many other areas. The problem of minimizing such objects can be traced back to …

Mirrors and Memory in Quantum Automata

In this paper we start from the simplest form of Quantum Finite Automata (QFAs), namely Measure-Once QFAs with cut-point. First we elaborate on a variant of their semantics that can be obtained through a shift from the Schrödinger to the Heisenberg …

Modeling and Solving the Rush Hour puzzle

We introduce the physical puzzle Rush Hour and its generalization. We briefly survey its complexity limits, then we model and solve it using declarative paradigms. In particular, we provide a constraint programming encoding in MiniZinc and a model in …

A Calculus for Attribute-Based Memory Updates

A time-series classification approach to shallow web traffic de-anonymization

Web traffic analysis and classification has been extensively studied, both with classical and deep learning techniques. Many of these systems analyse the entire packet to perform the classification task. Due to the increase of encrypted traffic in …

Automated symbolic verification of Telegram’s MTProto 2.0

MTProto 2.0 is a suite of cryptographic protocols for instant messaging at the core of the popular Telegram messenger application. In this paper we analyse MTProto 2.0 using the symbolic verifier ProVerif. We provide fully automated proofs of the …

Closure hyperdoctrines

(Pre)closure spaces are a generalization of topological spaces covering also the notion of neighbourhood in discrete structures, widely used to model and reason about spatial aspects of distributed systems. In this paper we present an abstract …

Composable Partial Multiparty Session Types

We introduce partial sessions and partial (multiparty) session types, in order to deal with open systems, i.e., systems with missing components. Partial sessions can be composed, and the type of the resulting system is derived from those of its …

Multi-agent Epistemic Planning with Inconsistent Beliefs, Trust and Lies

Developing autonomous agents that can reason about the perspective of their (human or artificial) peers is paramount to realistically model a variety of real-world domains. Being aware of the state of mind of others is a key aspect in different …

On the Security and Safety of AbU Systems

Attribute-based memory updates (AbU in short) is an interaction mechanism recently introduced for adapting the Event-Condition-Action (ECA) programming paradigm to distributed systems, particularly suited for the IoT. It can be seen as a memory-based …