Temporal Logics Over Finite Traces with Uncertainty (Technical Report)
Temporal logics over finite traces have recently seen wide application in a number of areas, from business process modelling, monitoring, and mining to planning and decision making. However, real-life dynamic systems contain a degree of uncertainty which cannot be handled with classical logics. We thus propose a new probabilistic temporal logic over finite traces using superposition semantics, where all possible evolutions are possible, until observed. We study the properties of the logic and provide automata-based mechanisms for deriving probabilistic inferences from its formulas. We then study a fragment of the logic with better computational properties. Notably, formulas in this fragment can be discovered from event log data using off-the-shelf existing declarative process discovery techniques.
Code (0)
등록된 구현이 없습니다.
Tasks
Decision MakingSimilar Papers 제목 키워드 기반
LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces
We introduce LTLf+ and PPLTL+, two logics to express properties of infinite traces, that are based on the linear-time temporal logics LTLf and PPLTL on finite traces. LTLf+/PPLTL+ use levels of Manna and Pnueli's LTL saf…
Past-present temporal programs over finite traces
Extensions of Answer Set Programming with language constructs from temporal logics, such as temporal equilibrium logic over finite traces (TELf), provide an expressive computational framework for modeling dynamic applica…
Implementing Dynamic Answer Set Programming
We introduce an implementation of an extension of Answer Set Programming (ASP) with language constructs from dynamic (and temporal) logic that provides an expressive computational framework for modeling dynamic applicati…
TranslationMonitoring Second-Order Hyperproperties
Hyperproperties express the relationship between multiple executions of a system. This is needed in many AI-related fields, such as knowledge representation and planning, to capture system properties related to knowledge…
Specifying Non-Markovian Rewards in MDPs Using LDL on Finite Traces (Preliminary Version)
In Markov Decision Processes (MDPs), the reward obtained in a state depends on the properties of the last state and action. This state dependency makes it difficult to reward more interesting long-term behaviors, such as…