1 Correction to: Innovations in Systems and Software Engineering https://doi.org/10.1007/s11334-022-00445-7
In the original publication of the article, the following corrections have been updated.
2 Introduction
Is:
Anzeige
Dedicated translations from LTL directly to (limit) deterministic [21] and unambiguous [25] automata have been studied.
Should be:
Dedicated translations from LTL directly to (limit-) deterministic [21] and unambiguous [25] automata have been studied.
3 In 3.1.1, Definition 3.3
Is:
Anzeige
Figure 3 is inside Definition 3.3, and breaks a list of items.
Should be:
Figure 3 should be outside of Definition 3.3., e.g., directly following it.
4 In 5.2: Proof of Proposition 5.3
Is:
In NP for limit-det. TELA. We now show that the problem of computing \(\textbf{Pr}_{\mathcal {M}}^{\max }(\mathcal {L}(\mathcal {A})) > 0\) is in NP if TELA \(\mathcal {A} = (Q,\Sigma ,\delta ,I,\alpha )\) is limit-deterministic.
[\(\ldots \)]
Claim. \(\textbf{Pr}^{\max }_{\mathcal {M}}(\mathcal {L}(\mathcal {A})) > 0\) holds iff there exists a reachable end-component \(\mathcal E\) of \(\mathcal {M}\times \mathcal {A}\) such that \({{\,\textrm{atrans}\,}}(\mathcal{E}) \models \alpha \).
[\(\ldots \)]
In P for fin-less limit-det. TELA. If \(\alpha \) is fin-less, then the existence of an end-component \(\mathcal E\) with \({{\,\textrm{atrans}\,}}(\mathcal{E}) \models \alpha \) is equivalent to the existence of a maximal end-component satisfying the same property.
Should be:
In NP for limit-det. TELA. We now show that the problem of computing \(\textbf{Pr}_{\mathcal {M}}^{\max }(\mathcal {L}(\mathcal {A})) > 0\) is in NP if TELA \(\mathcal {A} = (Q,\Sigma ,\delta ,I,\alpha )\) is limit-deterministic.
[\(\ldots \)]
Claim. \(\textbf{Pr}^{\max }_{\mathcal {M}}(\mathcal {L}(\mathcal {A})) > 0\) holds iff there exists a reachable end-component \(\mathcal E\) of \(\mathcal {M}\times \mathcal {A}\) such that \({{\,\textrm{atrans}\,}}(\mathcal{E}) \models \alpha \).
[\(\ldots \)]
In P for fin-less limit-det. TELA. If \(\alpha \) is fin-less, then the existence of an end-component \(\mathcal E\) with \({{\,\textrm{atrans}\,}}(\mathcal{E}) \models \alpha \) is equivalent to the existence of a maximal end-component satisfying the same property.
5 Sec 5.2: between Lemma 5.5 and Lemma 5.6
Is:
[\(\ldots \)] and show that words labeling a loop in the deterministic automaton \(\mathscr {D}_i\) induce a path through the powerset automaton of [\(\ldots \)]
Should be:
[\(\ldots \)] and show that words labeling a loop in the deterministic automaton \(\mathcal {D}_i\) induce a path through the powerset automaton of [\(\ldots \)]
Is:
Recall that we are given a finite memory scheduler \(\mathfrak {S}\) of \(\mathcal {M}\), and to prove the GFM property, we have to provide a scheduler \(\mathfrak {S}'\) such that \(\textrm{Pr}^{\mathfrak {S}}_{\mathcal {M}}(\mathcal {L}(\mathscr {A})) \le \textrm{Pr}^{\mathfrak {S}'}_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathscr {A}}}(\Pi _{acc})\). [\(\ldots \)] It stays inside the initial component of \(\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathscr {A}}\) and mimics the action chosen by \(\mathfrak {S}\) until the corresponding path in \(\mathcal {M}_{\mathfrak {S}} \times \mathcal {D}\) reaches an accepting bottom strongly connected component (BSCC) B.
Should be:
Recall that we are given a finite memory scheduler \(\mathfrak {S}\) of \(\mathcal {M}\), and to prove the GFM property, we have to provide a scheduler \(\mathfrak {S}'\) such that \(\textrm{Pr}^{\mathfrak {S}}_{\mathcal {M}}(\mathcal {L}(\mathcal {A})) \le \textrm{Pr}^{\mathfrak {S}'}_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}}(\Pi _{acc})\). [\(\ldots \)] It stays inside the initial component of \(\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}\) and mimics the action chosen by \(\mathfrak {S}\) until the corresponding path in \(\mathcal {M}_{\mathfrak {S}} \times \mathcal {D}\) reaches an accepting bottom strongly connected component (BSCC) B.
6 Sec 5.2: Lemma 5.6
Is:
Should be:
$$\begin{aligned} \textrm{Pr}_{s}(\{\pi \mid L(\pi ) \text { is accepted from } (Q',\varnothing ,0) \text { in } \mathfrak {B}_i\bigl \}) = 1. \end{aligned}$$
$$\begin{aligned} \textrm{Pr}_{\mathfrak {s}}(\{\pi \mid L(\pi ) \text { is accepted from } (Q',\varnothing ,0) \text { in } \mathfrak {B}_i\bigl \}) = 1. \end{aligned}$$
7 Sec 5.2: Lemma 5.7
Is:
Should be:
$$\begin{aligned} \mathop {\textrm{Pr}}_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}}^{\mathfrak {S}'}(\Pi _{acc}) \ge \mathop {\textrm{Pr}}_{\mathcal {M}}^{\mathfrak {S}}(\mathcal {L}(\mathcal {A})) \end{aligned}$$
$$\begin{aligned} \textrm{Pr}_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}}^{\mathfrak {S}'}(\Pi _{acc}) \ge \textrm{Pr}_{\mathcal {M}}^{\mathfrak {S}}(\mathcal {L}(\mathcal {A})) \end{aligned}$$
8 Sec 5.2: Theorem 5.2
Is:
Should be:
1.
For every finite memory scheduler \(\mathfrak {S}\) of \(\mathcal {M}\) there exists a scheduler \(\mathfrak {S}'\) of \(\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}\) such that
$$\begin{aligned} \mathop {\textrm{Pr}}^{\mathfrak {S}}_{\mathcal {M}}(\mathcal {L}(\mathcal {A})) \le \mathop {\textrm{Pr}}^{\mathfrak {S}'}_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}}(\Pi _{acc}) \end{aligned}$$
2.
For every finite memory scheduler \(\mathfrak {S}\) of \(\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}\) there exists a scheduler \(\mathfrak {S}'\) of \(\mathcal {M}\) such that
$$\begin{aligned} \mathop {\textrm{Pr}}^{\mathfrak {S}}_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}}(\Pi _{acc}) \le \mathop {\textrm{Pr}}^{\mathfrak {S}'}_{\mathcal {M}}(\mathcal {L}(\mathcal {A})) \end{aligned}$$
1.
For every finite memory scheduler \(\mathfrak {S}\) of \(\mathcal {M}\) there exists a scheduler \(\mathfrak {S}'\) of \(\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}\) such that
$$\begin{aligned} \textrm{Pr}^{\mathfrak {S}}_{\mathcal {M}}(\mathcal {L}(\mathcal {A})) \le \textrm{Pr}^{\mathfrak {S}'}_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}}(\Pi _{acc}) \end{aligned}$$
2.
For every finite memory scheduler \(\mathfrak {S}\) of \(\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}\) there exists a scheduler \(\mathfrak {S}'\) of \(\mathcal {M}\) such that
$$\begin{aligned} \textrm{Pr}^{\mathfrak {S}}_{\mathcal {M}\times \mathcal {G}^{{\text {GFM}}}_{\mathcal {A}}}(\Pi _{acc}) \le \textrm{Pr}^{\mathfrak {S}'}_{\mathcal {M}}(\mathcal {L}(\mathcal {A})) \end{aligned}$$
9 Sec 6: Table 1, first column (“Algorithm”)
Is:
Should be:
-
Spot
-
remFin\(\rightarrow \)split\(\alpha \)
-
split\(\alpha \) \(\rightarrow \)remFin
-
remFin\(\rightarrow \)rewrite\(\alpha \)
-
product
-
product (no langcover)
-
limit-det.
-
limit-det. via GBA
-
good-for-MDP
-
good-for-MDP via GBA
-
Spot
-
product
-
Spot -
remFin\(\rightarrow \)split\(\alpha \) -
split\(\alpha \rightarrow \)remFin -
remFin\(\rightarrow \)rewrite -
product -
product (no langcover) -
limit-det. -
limit-det. via GBA -
good-for-MDP -
good-for-MDP via GBA -
Spot -
product
10 Sec 6: Table 1
Should be:
-
the horizontal line after the 6th line shold not cross through the first column
-
random in the first column should be vertically aligned in the middle of the first 10 lines
Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.