Search

• < Previous
• 1
• Next >

---

Path Checking for MTL and TPTL over Data Words

Shiguang Feng ; Markus Lohrey ; Karin Quaas.

Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are quantitative extensions of linear temporal logic, which are prominent and widely used in the verification of real-timed systems. It was recently shown that the path checking problem for MTL, when evaluated over finite&nbsp;[&hellip;]

---

Capturing the polynomial hierarchy by second-order revised Krom logic

Kexu Wang ; Shiguang Feng ; Xishun Zhao.

We study the expressive power and complexity of second-order revised Krom logic (SO-KROM$^{r}$). On ordered finite structures, we show that its existential fragment $\Sigma^1_1$-KROM$^r$ equals $\Sigma^1_1$-KROM, and captures NL. On all finite structures, for $k\geq 1$, we show that $\Sigma^1_{k}$&nbsp;[&hellip;]

---