arXiv subjects

Elli Anastasiadi

Publications and source records attributed to Elli Anastasiadi.

8 recordsLinked to original sources

arXiv2026

The complexity of verifying the release-acquire semantics over register machines

The Release-Acquire (RA) semantics and its variants are some of the most fundamental models of concurrent semantics for architectures, programming languages, and distributed systems. Several steps have been taken in the direction of testing such semantics, where one is interested in whether a single program execution is consistent with a memory model. The more general verification problem, i.e., checking whether any allowed program run is consistent with a memory model, has still not been studied as much. The purpose of this work is to bridge this gap. We tackle the verification problem, where, given an implementation described as a register machine, we check if any of its runs violates the RA semantics or its Strong (SRA) and Weak (WRA) variants. We show that verifying WRA in this setup is in O(n5 ), while verifying the RA and SRA is PSPACE complete. This both answers some fundamental questions about the complexity of these problems, but also provides insights on the expressive power of register machines as a model.

cs.PL↗

arXiv2025

Centralized vs Decentralized Monitors for Hyperproperties

This paper focuses on the runtime verification of hyperproperties expressed in Hyper-recHML, an expressive yet simple logic for describing properties of sets of traces. To this end, we consider a simple language of monitors that observe sets of system executions and report verdicts w.r.t. a given Hyper-recHML formula. We first employ a unique omniscient monitor that centrally observes all system traces. Since centralised monitors are not ideal for distributed settings, we also provide a language for decentralized monitors, where each trace has a dedicated monitor; these monitors yield a unique verdict by communicating their observations to one another. For both the centralized and the decentralized settings, we provide a synthesis procedure that, given a formula, yields a monitor that is correct (i.e., sound and violation complete). A key step in proving the correctness of the synthesis for decentralized monitors is a result showing that, for each formula, the synthesized centralized monitor and its corresponding decentralized one are weakly bisimilar for a suitable notion of weak bisimulation.

cs.LO↗

arXiv2024

Complexity results for modal logic with recursion via translations and tableaux

This paper studies the complexity of classical modal logics and of their extension with fixed-point operators, using translations to transfer results across logics. In particular, we show several complexity results for multi-agent logics via translations to and from the $μ$-calculus and modal logic, which allow us to transfer known upper and lower bounds. We also use these translations to introduce terminating and non-terminating tableau systems for the logics we study, based on Kozen's tableau for the $μ$-calculus and the one of Fitting and Massacci for modal logic. Finally, we describe these tableaux with $μ$-calculus formulas, thus reducing the satisfiability of each of these logics to the satisfiability of the $μ$-calculus, resulting in a general 2EXP upper bound for satisfiability testing.

cs.LO↗

arXiv2022

Complexity through Translations for Modal Logic with Recursion

cs.LO↗

arXiv2022

Axiomatizing recursion-free, regular monitors

Monitors are a key tool in the field of runtime verification, where they are used to verify system properties by analyzing execution traces generated by processes. Work on runtime monitoring carried out in a series of papers by Aceto et al.$~$has specified monitors using a variation on the regular fragment of Milner's CCS and studied two trace-based notions of equivalence over monitors, namely verdict and $ω$-verdict equivalence. This article is devoted to the study of the equational logic of monitors modulo those two notions of equivalence. It presents complete equational axiomatizations of verdict and $ω$-verdict equivalence for closed and open terms over recursion-free monitors. It is also shown that verdict equivalence has no finite equational axiomatization over open monitors when the set of actions is finite and contains at least two actions.

cs.LO↗

arXiv2022

Monitoring hyperproperties with circuits

This paper presents an extension of the safety fragment of Hennessy-Milner Logic with recursion over sets of traces, in the spirit of Hyper-LTL. It then introduces a novel monitoring setup that employs circuit-like structures to combine verdicts from regular monitors. The main contribution of this study is the monitors and their semantics themselves, as well as a monitor-synthesis procedure from formulae in the logic that yields `circuit-like monitors' of this type that are sound and violation complete over a finite set of infinite traces.

cs.LO↗

arXiv2021

In search of lost time: Axiomatising parallel composition in process algebras

This survey reviews some of the most recent achievements in the saga of the axiomatisation of parallel composition, along with some classic results. We focus on the recursion, relabelling and restriction free fragment of CCS and we discuss the solutions to three problems that were open for many years. The first problem concerns the status of Bergstra and Klop's auxiliary operators left merge and communication merge in the finite axiomatisation of parallel composition modulo bisimiliarity: We argue that, under some natural assumptions, the addition of a single auxiliary binary operator to CCS does not yield a finite axiomatisation of bisimilarity. Then we delineate the boundary between finite and non-finite axiomatisability of the congruences in van Glabbeek's linear time-branching time spectrum over CCS. Finally, we present a novel result to the effect that rooted weak bisimilarity has no finite complete axiomatisation over CCS.

cs.LO↗

arXiv2019

Parameterized Fine-Grained Reductions

During recent years the field of fine-grained complexity has bloomed to produce a plethora of results, with both applied and theoretical impact on the computer science community. The cornerstone of the framework is the notion of fine-grained reductions, which correlate the exact complexities of problems such that improvements in their running times or hardness results are carried over. We provide a parameterized viewpoint of these reductions (PFGR) in order to further analyze the structure of improvable problems and set the foundations of a unified methodology for extending algorithmic results. In this context, we define a class of problems (FPI) that admit fixed-parameter improvements on their running time. As an application of this framework we present a truly sub-quadratic fixed-parameter algorithm for the orthogonal vectors problem. Finally, we provide a circuit characterization for FPI to further solidify the notion of improvement.

cs.CC↗