5 accepted papers
We study monitoring of linear-time arithmetic properties against finite traces generated by an unknown dynamic system. The monitoring state is determined by considering at once the trace prefix seen so far, and all its possible finite-length, future continuations. This makes monitoring at least as h…
Combined modeling and verification of dynamic systems and the data they operate on has gained momentum in AI and in several application domains. We investigate the expressive yet concise framework of data-aware dynamic systems (DDS), extending it with linear arithmetic, and providing the following c…
Manufacturing is transitioning from a mass production model to a service model in which facilities `bid' for previously unseen products. To decide whether to bid for a previously unseen product, a facility must be able to synthesize, on the fly, a process plan controller that delegates abstract manu…
Temporal logics over finite traces, such as LTLf and its extension LDLf, have been adopted in several areas, including Business Process Management (BPM), to check properties of processes whose executions have an unbounded, but finite, length. These logics express properties of single traces in isol…
We study the problem of verifying whether a given parameterized multi-agent system (PMAS) is safe, namely whether none of its possible executions can lead to bad states. These are captured by a state formula existentially quantifying over agents. As the MAS is parameterized, it only describes the fi…