arXiv subjects

Flavio Ferrarotti

Publications and source records attributed to Flavio Ferrarotti.

At least 19 recordsLinked to original sources

arXiv2026

A Behavioural Theory of Probabilistic Algorithms Using Probabilistic Abstract State Machines

We motivate an axiomatic definition of probabilistic algorithms (PAs) by four postulates covering random branching time, abstract states, background, and random bounded exploration. Then, we introduce probabilistic Abstract State Machines (pASMs) and show that they specify PAs. Finally, we prove that every PA satisfying these postulates can be simulated step-by-step by a behaviourally equivalent pASM with the same signature and background.

cs.LO↗

arXiv2026

Software-Hardware Binding for Protection of Sensitive Data in Embedded Software

Embedded software used in industrial systems frequently relies on data that ensures the correct and efficient operation of these systems. Thus, companies invest considerable resources in fine-tuning this data, making it their valuable intellectual property (IP). We present a novel protection mechanism for this IP that combines hardware fingerprints with Boolean logic. Unlike usual copy-protection approaches, unauthorised copies of the software still run on cloned devices but suboptimally. According to our security evaluation, only a complex dynamic analysis of the protected software running on the genuine target device can reveal the secret data. This makes the protection offered by our method more difficult to bypass. Notably, our approach does not require additional hardware, relying only on relatively simple updates to the software. We evaluate our protection mechanism by binding the parameters of a PID controller to a microcontroller unit (MCU) by using a physically unclonable function (PUF) based on its SRAM.

cs.CR↗

arXiv2026

An Approach for Safe and Secure Software Protection Supported by Symbolic Execution

We introduce a novel copy-protection method for industrial control software. With our method, a program executes correctly only on its target hardware and behaves differently on other machines. The hardware-software binding is based on Physically Unclonable Functions (PUFs). We use symbolic execution to guarantee the preservation of safety properties if the software is executed on a different machine, or if there is a problem with the PUF response. Moreover, we show that the protection method is also secure against reverse engineering.

cs.CR↗

arXiv2026

A PUF-Based Approach for Copy Protection of Intellectual Property in Neural Network Models

More and more companies' Intellectual Property (IP) is being integrated into Neural Network (NN) models. This IP has considerable value for companies and, therefore, requires adequate protection. For example, an attacker might replicate a production machines' hardware and subsequently simply copy associated software and NN models onto the cloned hardware. To make copying NN models onto cloned hardware infeasible, we present an approach to bind NN models - and thus also the IP contained within them - to their underlying hardware. For this purpose, we link an NN model's weights, which are crucial for its operation, to unique and unclonable hardware properties by leveraging Physically Unclonable Functions (PUFs). By doing so, sufficient accuracy can only be achieved using the target hardware to restore the original weights, rendering proper execution of the NN model on cloned hardware impossible. We demonstrate that our approach accomplishes the desired degradation of accuracy on various NN models and outline possible future improvements.

cs.CR↗

arXiv2025

TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory

The verification of liveness conditions is an important aspect of state-based rigorous methods. This article addresses the extension of the logic of Event-B to a powerful logic, in which properties of traces of an Event-B machine can be expressed. However, all formulae of this logic are still interpreted over states of an Event-B machine rather than traces. The logic exploits that for an Event-B machine $M$ a state $S$ determines all traces of $M$ starting in $S$. We identify a fragment called TREBL of this logic, in which all liveness conditions of interest can be expressed, and define a set of sound derivation rules for the fragment. We further show relative completeness of these derivation rules in the sense that for every valid entailment of a formula $\varphi$ one can find a derivation, provided the machine $M$ is sufficiently refined. The decisive property is that certain variant terms must be definable in the refined machine. We show that such refinements always exist. Throughout the article several examples from the field of security are used to illustrate the theory.

cs.LO↗

arXiv2025

Behavioural Theory of Reflective Algorithms II: Reflective Parallel Algorithms

We develop a behavioural theory of reflective parallel algorithms (RAs), i.e. synchronous parallel algorithms that can modify their own behaviour. The theory comprises a set of postulates defining the class of RAs, an abstract machine model, and the proof that all RAs are captured by this machine model. RAs are sequential-time, parallel algorithms, where every state includes a representation of the algorithm in that state, thus enabling linguistic reflection. Bounded exploration is preserved using multiset comprehension terms as values. The abstract machine model is defined by reflective Abstract State Machines (rASMs), which extend ASMs using extended states that include an updatable representation of the main ASM rule to be executed by the machine in that state.

cs.LO↗

arXiv2024

A Complete Fragment of LTL(EB)

The verification of liveness conditions is an important aspect of state-based rigorous methods. This article investigates this problem in a fragment $\square$LTL of the logic LTL(EB), the integration of the UNTIL-fragment of Pnueli's linear time temporal logic (LTL) and the logic of Event-B, in which the most commonly used liveness conditions can be expressed. For this fragment a sound set of derivation rules is developed, which is also complete under mild restrictions for Event-B machines.

cs.LO↗

arXiv2024

Choiceless Polynomial Space

Abstract State Machines (ASMs) provide a model of computations on structures rather than strings. Blass, Gurevich and Shelah showed that deterministic PTIME-bounded ASMs define the choiceless fragment of PTIME, but cannot capture PTIME. In this article deterministic PSPACE-bounded ASMs are introduced, and it is proven that they cannot capture PSPACE. The key for the proof is a characterisation by partial fixed-point formulae over the St\"ark/Nanchen logic for deterministic ASMs and a construction of transitive structures, in which such formulae must hold. This construction exploits that the decisive support theorem for choiceless polynomial time holds under slightly weaker assumptions.

cs.LO↗

arXiv2020

Completeness in Polylogarithmic Time and Space

Complexity theory can be viewed as the study of the relationship between computation and applications, understood the former as complexity classes and the latter as problems. Completeness results are clearly central to that view. Many natural algorithms resulting from current applications have polylogarithmic time (PolylogTime) or space complexity (PolylogSpace). The classical Karp notion of complete problem however does not plays well with these complexity classes. It is well known that PolylogSpace does not have complete problems under logarithmic space many-one reductions. In this paper we show similar results for deterministic and non-deterministic PolylogTime as well as for every other level of the polylogarithmic time hierarchy. We achieve that by following a different strategy based on proving the existence of proper hierarchies of problems inside each class. We then develop an alternative notion of completeness inspired by the concept of uniformity from circuit complexity and prove the existence of a (uniformly) complete problem for PolylogSpace under this new notion. As a consequence of this result we get that complete problems can still play an important role in the study of the interrelationship between polylogarithmic and other classical complexity classes.

cs.LO↗

arXiv2020

Behavioural Theory of Reflective Algorithms I: Reflective Sequential Algorithms

We develop a behavioural theory of reflective sequential algorithms (RSAs), i.e. sequential algorithms that can modify their own behaviour. The theory comprises a set of language-independent postulates defining the class of RSAs, an abstract machine model, and the proof that all RSAs are captured by this machine model. As in Gurevich's behavioural theory for sequential algorithms RSAs are sequential-time, bounded parallel algorithms, where the bound depends on the algorithm only and not on the input. Different from the class of sequential algorithms every state of an RSA includes a representation of the algorithm in that state, thus enabling linguistic reflection. Bounded exploration is preserved using terms as values. The model of reflective sequential abstract state machines (rsASMs) extends sequential ASMs using extended states that include an updatable representation of the main ASM rule to be executed by the machine in that state. Updates to the representation of ASM signatures and rules are realised by means of a sophisticated tree algebra.

cs.LO↗

arXiv2019

Descriptive Complexity of Deterministic Polylogarithmic Time and Space

We propose logical characterizations of problems solvable in deterministic polylogarithmic time (PolylogTime) and polylogarithmic space (PolylogSpace). We introduce a novel two-sorted logic that separates the elements of the input domain from the bit positions needed to address these elements. We prove that the inflationary and partial fixed point vartiants of this logic capture PolylogTime and PolylogSpace, respectively. In the course of proving that our logic indeed captures PolylogTime on finite ordered structures, we introduce a variant of random-access Turing machines that can access the relations and functions of a structure directly. We investigate whether an explicit predicate for the ordering of the domain is needed in our PolylogTime logic. Finally, we present the open problem of finding an exact characterization of order-invariant queries in PolylogTime.

cs.LO↗

arXiv2019

Proper Hierarchies in Polylogarithmic Time and Absence of Complete Problems

The polylogarithmic time hierarchy structures sub-linear time complexity. In recent work it was shown that all classes $\tildeΣ_{m}^{\mathit{plog}}$ or $\tildeΠ_{m}^{\mathit{plog}}$ ($m \in \mathbb{N}$) in this hierarchy can be captured by semantically restricted fragments of second-order logic. In this paper the descriptive complexity theory of polylogarithmic time is taken further showing that there are strict hierarchies inside each of the classes of the hierarchy. A straightforward consequence of this result is that there are no complete problems for these complexity classes, not even under polynomial time reductions. As another consequence we show that the polylogarithmic time hierarchy itself is strict.

cs.CC↗

arXiv2019

A Restricted Second-Order Logic for Non-deterministic Poly-Logarithmic Time

We introduce a restricted second-order logic $\mathrm{SO}^{\mathit{plog}}$ for finite structures where second-order quantification ranges over relations of size at most poly-logarithmic in the size of the structure. We demonstrate the relevance of this logic and complexity class by several problems in database theory. We then prove a Fagin's style theorem showing that the Boolean queries which can be expressed in the existential fragment of $\mathrm{SO}^{\mathit{plog}}$ corresponds exactly to the class of decision problems that can be computed by a non-deterministic Turing machine with random access to the input in time $O((\log n)^k)$ for some $k \ge 0$, i.e., to the class of problems computable in non-deterministic poly-logarithmic time. It should be noted that unlike Fagin's theorem which proves that the existential fragment of second-order logic captures NP over arbitrary finite structures, our result only holds over ordered finite structures, since $\mathrm{SO}^{\mathit{plog}}$ is too weak as to define a total order of the domain. Nevertheless $\mathrm{SO}^{\mathit{plog}}$ provides natural levels of expressibility within poly-logarithmic space in a way which is closely related to how second-order logic provides natural levels of expressibility within polynomial space. Indeed, we show an exact correspondence between the quantifier prefix classes of $\mathrm{SO}^{\mathit{plog}}$ and the levels of the non-deterministic poly-logarithmic time hierarchy, analogous to the correspondence between the quantifier prefix classes of second-order logic and the polynomial-time hierarchy. Our work closely relates to the constant depth quasipolynomial size AND/OR circuits and corresponding restricted second-order logic defined by David A. Mix Barrington in 1992. We explore this relationship in detail.

cs.LO↗

arXiv2018

The Polylog-Time Hierarchy Captured by Restricted Second-Order Logic

Let $\mathrm{SO}^{\mathit{plog}}$ denote the restriction of second-order logic, where second-order quantification ranges over relations of size at most poly-logarithmic in the size of the structure. In this article we investigate the problem, which Turing machine complexity class is captured by Boolean queries over ordered relational structures that can be expressed in this logic. For this we define a hierarchy of fragments $Σ^{\mathit{plog}}_m$ (and $Π^{\mathit{plog}}_m$) defined by formulae with alternating blocks of existential and universal second-order quantifiers in quantifier-prenex normal form. We first show that the existential fragment $Σ^{\mathit{plog}}_1$ captures NPolyLogTime, i.e. the class of Boolean queries that can be accepted by a non-deterministic Turing machine with random access to the input in time $O((\log n)^k)$ for some $k \ge 0$. Using alternating Turing machines with random access input allows us to characterise also the fragments $Σ^{\mathit{plog}}_m$ (and $Π^{\mathit{plog}}_m$) as those Boolean queries with at most $m$ alternating blocks of second-order quantifiers that are accepted by an alternating Turing machine. Consequently, $\mathrm{SO}^{\mathit{plog}}$ captures the whole poly-logarithmic time hierarchy. We demonstrate the relevance of this logic and complexity class by several problems in database theory.

cs.LO↗

arXiv2018

Expressivity within second-order transitive-closure logic

Second-order transitive-closure logic, SO(TC), is an expressive declarative language that captures the complexity class PSPACE. Already its monadic fragment, MSO(TC), allows the expression of various NP-hard and even PSPACE-hard problems in a natural and elegant manner. As SO(TC) offers an attractive framework for expressing properties in terms of declaratively specified computations, it is interesting to understand the expressivity of different features of the language. This paper focuses on the fragment MSO(TC), as well on the purely existential fragment SO(2TC)(E); in 2TC, the TC operator binds only tuples of relation variables. We establish that, with respect to expressive power, SO(2TC)(E) collapses to existential first-order logic. In addition we study the relationship of MSO(TC) to an extension of MSO(TC) with counting features (CMSO(TC)) as well as to order-invariant MSO. We show that the expressive powers of CMSO(TC) and MSO(TC) coincide. Moreover we establish that, over unary vocabularies, MSO(TC) strictly subsumes order-invariant MSO.

cs.LO↗

arXiv2017

A Complete Logic for Database Abstract State Machines

In database theory, the term $\textit{database transformation}$ was used to refer to a unifying treatment for computable queries and updates. Recently, it was shown that non-deterministic database transformations can be captured exactly by a variant of ASMs, the so-called Database Abstract State Machines (DB-ASMs). In this article we present a logic for DB-ASMs, extending the logic of Nanchen and Stärk for ASMs. In particular, we develop a rigorous proof system for the logic for DB-ASMs, which is proven to be sound and complete. The most difficult challenge to be handled by the extension is a proper formalisation capturing non-determinism of database transformations and all its related features such as consistency, update sets or multisets associated with DB-ASM rules. As the database part of a state of database transformations is a finite structure and DB-ASMs are restricted by allowing quantifiers only over the database part of a state, we resolve this problem by taking update sets explicitly into the logic, i.e. by using an additional modal operator $[X]$, where $X$ is interpreted as an update set $Δ$ generated by a DB-ASM rule. The DB-ASM logic provides a powerful verification tool to study properties of database transformations.

cs.LO↗

arXiv2017

A Logic for Non-Deterministic Parallel Abstract State Machines

We develop a logic which enables reasoning about single steps of non-deterministic parallel Abstract State Machines (ASMs). Our logic builds upon the unifying logic introduced by Nanchen and Stärk for reasoning about hierarchical (parallel) ASMs. Our main contribution to this regard is the handling of non-determinism (both bounded and unbounded) within the logical formalism. Moreover, we do this without sacrificing the completeness of the logic for statements about single steps of non-deterministic parallel ASMs, such as invariants of rules, consistency conditions for rules, or step-by-step equivalence of rules.

cs.LO↗

arXiv2017

Towards an ASM thesis for reflective sequential algorithms

Starting from Gurevich's thesis for sequential algorithms (the so-called "sequential ASM thesis"), we propose a characterization of the behaviour of sequential algorithms enriched with reflection. That is, we present a set of postulates which we conjecture capture the fundamental properties of reflective sequential algorithms (RSAs). Then we look at the plausibility of an ASM thesis for the class of RSAs, defining a model of abstract state machine (which we call reflective ASM) that we conjecture captures the class of RSAs as defined by our postulates.

cs.LO↗