LTLf and LDLf Monitoring: A Technical Report
Runtime monitoring is one of the central tasks to provide operational decision support to running business processes, and check on-the-fly whether they comply with constraints and rules. We study runtime monitoring of properties expressed in LTL on finite traces (LTLf) and in its extension LDLf. LDLf is a powerful logic that captures all monadic second order logic on finite traces, which is obtained by combining regular expressions and LTLf, adopting the syntax of propositional dynamic logic (PDL). Interestingly, in spite of its greater expressivity, LDLf has exactly the same computational complexity of LTLf. We show that LDLf is able to capture, in the logic itself, not only the constraints to be monitored, but also the de-facto standard RV-LTL monitors. This makes it possible to declaratively capture monitoring metaconstraints, and check them by relying on usual logical services instead of ad-hoc algorithms. This, in turn, enables to flexibly monitor constraints depending on the monitoring state of other constraints, e.g., "compensation" constraints that are only checked when others are detected to be violated. In addition, we devise a direct translation of LDLf formulas into nondeterministic automata, avoiding to detour to Buechi automata or alternating automata, and we use it to implement a monitoring plug-in for the PROM suite.
Code (0)
등록된 구현이 없습니다.
Tasks
TranslationSimilar Papers 제목 키워드 기반
Foundations for Restraining Bolts: Reinforcement Learning with LTLf/LDLf restraining specifications
In this work we investigate on the concept of "restraining bolt", envisioned in Science Fiction. Specifically we introduce a novel problem in AI. We have two distinct sets of features extracted from the world, one by the…
reinforcement-learningReinforcement LearningReinforcement Learning (RL)Planning and Synthesis Under Assumptions
In Reasoning about Action and Planning, one synthesizes the agent plan by taking advantage of the assumption on how the environment works (that is, one exploits the environment's effects, its fairness, its trajectory con…
FairnessFOND Planning for LTLf and PLTLf Goals
In this report, we will define a new approach to the problem of non deterministic planning for extended temporal goals. In particular, we will give a solution to this problem reducing it to a fully observable non determi…
Computing unsatisfiable cores for LTLf specifications
Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains (e.g., planning, business process management, run-time monitoring, reactive…
ManagementMonitoring Data-aware Temporal Properties (Extended Version)
Dynamic systems in AI are often complex and heterogeneous, so that an internal specification is not accessible and verification techniques such as model checking are not applicable. Monitoring is in such cases an attract…