8 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…
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…
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…
If At First You Don't Succeed: Extended Monitorability through Multiple Executions
Antonis Achilleos, Adrian Francalanza, Jasmine Xuereb
This paper studies the extent to which branching-time properties can be adequately verified using runtime monitors. We depart from the classical setup where monitoring is limited t…
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…