9 papers
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…
Denotational Semantics for Probabilistic and Concurrent Programs
Noam Zilberstein, Daniele Gorla, Alexandra Silva
We develop a denotational model for probabilistic and concurrent imperative programs, a class of programs with standard control flow via conditionals and while-loops, as well as pr…
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…