45 citations · 74 across the 16 of their papers we have counts for
17 papers · 1 filter
A Behavioural Theory of Probabilistic Algorithms Using Probabilistic Abstract State Machines
Flavio Ferrarotti, Klaus-Dieter Schewe
We motivate an axiomatic definition of probabilistic algorithms (PAs) by four postulates covering random branching time, abstract states, background, and random bounded exploration…
TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory
Klaus-Dieter Schewe, Flavio Ferrarotti, Peter Rivière +3
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…
Behavioural Theory of Reflective Algorithms II: Reflective Parallel Algorithms
Klaus-Dieter Schewe, Flavio Ferrarotti
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 pos…
A Complete Fragment of LTL(EB)
Flavio Ferrarotti, Peter Rivière, Klaus-Dieter Schewe +2
The verification of liveness conditions is an important aspect of state-based rigorous methods. This article investigates this problem in a fragment LTL of the logic LTL(E…
Choiceless Polynomial Space
Flavio Ferrarotti, Klaus-Dieter Schewe
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…
Completeness in Polylogarithmic Time and Space
Flavio Ferrarotti, Senen Gonzalez, Klaus-Dieter Schewe +1
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. Compl…
Behavioural Theory of Reflective Algorithms I: Reflective Sequential Algorithms
Klaus-Dieter Schewe, Flavio Ferrarotti
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-i…
A Restricted Second-Order Logic for Non-deterministic Poly-Logarithmic Time
Flavio Ferrarotti, Senen Gonzáles, Klaus-Dieter Schewe +1
We introduce a restricted second-order logic for finite structures where second-order quantification ranges over relations of size at most poly-logari…
Descriptive Complexity of Deterministic Polylogarithmic Time and Space
Flavio Ferrarotti, Senén González, José María Turull Torres +2
We propose logical characterizations of problems solvable in deterministic polylogarithmic time (PolylogTime) and polylogarithmic space (PolylogSpace). We introduce a novel two-sor…
The Polylog-Time Hierarchy Captured by Restricted Second-Order Logic
Flavio Ferrarotti, Senén González, Klaus-Dieter Schewe +1
Let denote the restriction of second-order logic, where second-order quantification ranges over relations of size at most poly-logarithmic in the size…
Expressivity within second-order transitive-closure logic
Flavio Ferrarotti, Jan Van den Bussche, Jonni Virtema
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 ex…
A Logic for Non-Deterministic Parallel Abstract State Machines
Flavio Ferrarotti, Klaus-Dieter Schewe, Loredana Tec +1
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 N…
Towards an ASM thesis for reflective sequential algorithms
Flavio Ferrarotti, Loredana Tec, Jose Maria Turull Torres
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…
On Higher Order Query Languages which on Relational Databases Collapse to Second Order Logic
Flavio Ferrarotti, Loredana Tec, José María Turull-Torres
In the framework of computable queries in Database Theory, there are many examples of queries to (properties of) relational database instances that can be expressed by simple and e…
A Complete Logic for Database Abstract State Machines
Flavio Ferrarotti, Klaus-Dieter Schewe, Loredana Tec +1
In database theory, the term was used to refer to a unifying treatment for computable queries and updates. Recently, it was shown that non-determ…
A New Thesis concerning Synchronised Parallel Computing - Simplified Parallel ASM Thesis
Flavio Ferrarotti, Klaus-Dieter Schewe, Loredana Tec +1
A behavioural theory consists of machine-independent postulates characterizing a particular class of algorithms or systems, an abstract machine model that provably satisfies these…
Expressing Properties in Second and Third Order Logic: Hypercube Graphs and SATQBF
F. Ferrarotti, W. Ren, J. M. Turull Torres
It follows from the famous Fagin's theorem that all problems in NP are expressible in existential second-order logic (ESO), and vice versa. Indeed, there are well-known ESO charact…