Title: Weighted linear dynamic logic with two-sorted semantics

In 2013 Giuseppe De Giacomo and Moshe Vardi introduced linear dynamic logic. This logic uses the intuitive, two-sorted syntax of PDL, has good complexity properties, and extends the expressive power of LTL: De Giacomo and Vardi prove LDL and finite automata are equally expressive. This is done via alternating automata. In 2016 Manfred Droste and George Rahonis introduced a weighted version of LDL with weights taken from semirings.

In this talk, I will introduce a new adaptation of LDL into the weighted setting. While weighted LDL uses generalized rational expressions in the definition of its semantics, nLDL mirrors the two-sorted semantics of LDL. This is to obtain an intuitive syntax similar to LDL. Moreover, nLDL is more expressive than weighted LDL, and relates to weighted LTL as LDL relates to LTL. I will show that, similar to PDL, the depth of the question-mark operator entails a hierarchy on the expressive power of nLDL. To characterize nLDL, I will introduce n-level weighted finite automata which are a subclass of nested weighted automata and capture the expressive power of nLDL.