40 citations · 42 across the 9 of their papers we have counts for
12 papers · 1 filter
A Topological Framework for Finite Behavioural Observations and Verification
Antonis Achilleos, Vasiliki Kyriakou
Formal verification and monitorability are based on finite observations, which allow properties to be verified from finite information about system behaviour. We study such observa…
An Undecidability Proof for the Plan Existence Problem
Antonis Achilleos
The plan existence problem asks, given a goal in the form of a formula in modal logic, an initial epistemic state (a pointed Kripke model), and a set of epistemic actions, whether…
Monitorability for the Modal mu-Calculus over Systems with Data: From Practice to Theory
Luca Aceto, Antonis Achilleos, Duncan Paul Attard +4
Runtime verification, also known as runtime monitoring, consists of checking whether a system satisfies a given specification by observing the trace it produces during its executio…
Deciding characteristic formulae: A journey in the branching-time spectrum
Luca Aceto, Antonis Achilleos, Aggeliki Chalki +1
Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence o…
The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrum
Luca Aceto, Antonis Achilleos, Aggeliki Chalki +1
Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence o…
Centralized vs Decentralized Monitors for Hyperproperties
Luca Aceto, Antonis Achilleos, Elli Anastasiadi +3
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…