text:
Search SpringerLink
Vacuity in synthesis
Roderick Bloem1,
Hana Chockler2,
Masoud Ebrahimi1 &
Ofer Strichman ORCID: orcid.org/0000-0001-9169-37513
Formal Methods in System Design volume 57, pages 473–495 (2021)Cite this article
In reactive synthesis, one begins with a temporal specification \(\varphi \), and automatically synthesizes a system \(M\) such that \(M\models \varphi \). As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies \(\varphi \) non-vacuously, then M is likely to be closer to the user's intent, because it satisfies \(\varphi \) in a more "meaningful" way. Narrowing the gap between the formal specification and the designer's intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.
Given a temporal specification \(\varphi \), the goal of reactive synthesis [9, 17] is to build a transition system M such that \(M \models \varphi \). The motivation of synthesis is clear: rather than building a design and then checking whether it adheres to the specification, focus on the specification alone, and generate automatically a design that satisfies it. In recent years, the theory and especially the tools for synthesis have made significant progress [11].
As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity [2]. It is a standard concept in model-checking, for detecting errors in the specification itself, the model, or both. So far it has not been used in the context of synthesis, however. Our conjecture is that if the synthesized system M satisfies \(\varphi \) non-vacuously, then M is likely to be closer to the user's intent, because it satisfies \(\varphi \) in a more "meaningful" way. Narrowing the gap between the formal specification and the designer's intent in this way, automatically, is the topic of this article.
Consider, for example, the property
$$\begin{aligned} \varphi = \text {{G}}(req \rightarrow \text {{F}}grant). \end{aligned}$$
A system M with one state satisfying grant (regardless of req) satisfies \(\varphi \), and is indeed a legitimate outcome of synthesising (1). However, M also satisfies stronger properties such as \(\text {{G}}\text {{F}}grant\). When a system satisfies a property regardless of some of its subformulas, as in this example where the behavior of req is immaterial for the satisfaction of \(\varphi \), the specification is said to be satisfied vacuously (see below a formal definition).
It is not likely that M captures the user's intent: the intent is probably that the system also permits a path \(\pi \) in which there are no grants from a point in which there are no requests. Such a path is called an interesting witness [2]: it is an execution that demonstrates non-vacuous satisfaction of the original property. However, the requirement that there exists an interesting witness cannot be expressed in LTL, since it implicitly relies on an existential quantifier.
Previous work addressing the lack of expressibility of LTL in specifying high-quality systems suggested the extension to quantitative specifications, in order to make it easier to specify certain properties [4], and to be able to synthesize systems that are robust against environment errors, even if the way to react to such errors has not been specified explicitly [3, 18].
There are multiple definitions of vacuity in the literature [1, 2, 6, 7, 14, 15]; the vast majority of them is based on the concept of strengthening the specification by changing a part of it and checking whether the strengthened version is still satisfied in the system; if not, then the system is considered to satisfy the specification non-vacuously. While the general method that we will describe in this paper is orthogonal to the chosen definition as long as the analysed formulas are still in LTL, for ease of exposition we will choose one definition and use it throughout the paper. Most commercially used vacuity-detection tools use the generalised definition by Kupferman and Vardi [14], which is what we will follow here: Let \(\psi \) be a subformula in \(\varphi \). The strengthening of \(\varphi \) with respect to \(\psi \) is \(\varphi [\psi \leftarrow \bot ]\).Footnote 1 If \(M \models \varphi [\psi \leftarrow \bot ]\) then \(\psi \) is irrelevant for the satisfaction of \(\varphi \) in M, and we say that \(\varphi \) is satisfied in M vacuously with respect to \(\psi \). It follows that M satisfies \(\varphi \) non-vacuously with respect to \(\psi \) iff \(M \models \text {{E}}\lnot \varphi [\psi \leftarrow \bot ]\). As shown in [14], it is sufficient to consider strengthenings of \(\varphi \) with respect to atomic propositions (literals, in fact) rather than all subformulas. We note that the definitions of vacuity in the literature, including [14], did not consider the division of the atomic propositions into inputs and outputs, as such division is immaterial in model-checking. As we argue later, in synthesis this division is in fact important.
Our synthesis method requires systems with at least one interesting witness for every possible strengthening of \(\varphi \). More formally, if \(\varphi \) is a specification in LTL, a model M satisfies \(\varphi \) non vacuously if it satisfies a formula in a simple fragment of CTL\(^*\) consisting of a conjunction of universal and existential formulas:
$$\begin{aligned} (M \models \text {{A}}\varphi ) \wedge \bigwedge _{\psi \in \text {Lit}\left( \varphi \right) } (M \models \text {{E}}\lnot \varphi [\psi \leftarrow \bot ])\;, \end{aligned}$$
where \(\text {Lit}\left( \varphi \right) \) denotes the literals of \(\varphi \). One of the contributions of this article is the extension of the bounded synthesis [10] algorithm to handle this fragment, based on a new ranking function (the original bounded synthesis algorithm handles only universal formulas).
Even when the system satisfies the specification non-vacuously, our tool is capable of improving it by synthesizing a system that has additional interesting witnesses. The users decides when the system reflects their intent. In Sect. 3 we define a partial order of vacuity on transition systems, stating that system \(M'\) is less vacuous than M if it contains all of the interesting witnesses permitted by M and at least one more. This condition can be stated as a formula in the same fragment of CTL\(^*\) mentioned above. We describe a synthesis procedure for generating increasingly non-vacuous systems for a given number of states.
In Sect. 4, we revisit the partial order of vacuity and prove that this partial order can be mapped to a partial order on subsets of input traces. This allows us to formally introduce the concept of equivalent systems w.r.t. their degree of vacuity and discuss cases where there is a single top element to the partial order of vacuity, multiple equivalent top elements, or multiple incomparable top elements. This is also the main addition to the paper compared to its conference version [5].
We have implemented the non-vacuous bounded synthesis algorithm on top of the PARTY synthesizer [13], which is available for download.Footnote 2 Given the informal goal we stated ("capturing the user's intent") naturally it is difficult to prove that our approach works, especially since there are no users in the industry that specify real system for the purpose of synthesis. Our experiments were based, then, on starting from previously published complete specifications, removing parts of them, and activating non-vacuous synthesis. In our experiments, which we describe in Sect. 5, the removed parts of the specification were compensated by our tool. In fact, the generated models not only satisfy the original, complete specifications, but they also realize them less vacuously.
Motivating example
The following example will be used in the rest of the article as a running example. It is a specification of an arbiter with two types of requests and two types of grants (i. e., \(\varphi _1\) and \(\varphi _2\)) and a mutual exclusion between the grants (i. e., \(\varphi _3\)). The specification \(\varphi \) is a conjunction of the following three properties:
$$\begin{aligned} \varphi _1 = \text {{G}}(r_1 \rightarrow \text {{F}}g_1)\;, \quad \varphi _2 =\text {{G}}(r_2 \rightarrow \text {{F}}g_2)\;, \quad \varphi _3 =\text {{G}}(\lnot (g_1 \wedge g_2))\;, \end{aligned}$$
where \(r_1\) and \(r_2\) are inputs (the 'requests') and \(g_1\) and \(g_2\) are outputs (the 'grants'). The smallest system \(M_0\) satisfying \(\varphi \), synthesised by our tool, is depicted in Fig. 1a. It consists of two states, \(s_0\) and \(s_1\), where in each state exactly one of the grants is up. It is easy to see that \(M_0\) satisfies \(\varphi \) vacuously. In particular \(M_0 \models \varphi _1[r_1 \leftarrow \bot ]\) and \(M_0 \models \varphi _2[r_2 \leftarrow \bot ]\), where the \(\bot \) value for \(r_1\) and \(r_2\) is \({\text {{true}}}\) in both \(\varphi _1\) and \(\varphi _2\), respectively.
Systems of the running example
The system generated by our tool in the next step is \(M_1\), depicted in Fig. 1b.Footnote 3 This system satisfies \(\varphi \) non-vacuously in all its subformulas. Indeed:
\(M_1 \not \models \varphi _1[r_1 \leftarrow \bot ]\), as the path \(\pi _1 = s_0^\omega \) corresponding to the output trace \(\{\lnot {g_1},g_2\}^\omega \) falsifies \(\text {{G}}\text {{F}}g_1\);
\(M_1 \not \models \varphi _2[r_2 \leftarrow \bot ]\), as the path \(\pi _2 = s_0 s_1^\omega \) corresponding to the output trace \(\{\lnot {g_1},g_2\},\{g_1,\lnot {g_2}\}^\omega \) falsifies \(\text {{G}}\text {{F}}g_2\);
The formulas obtained by replacing one of the grants with false are unrealisable, i. e., there is no system that can satisfy, for example, \(\text {{G}}(\lnot {r_1})\), because we have no control over the inputs.
\(\square \)
Preliminaries
Labeled transition systems
For the remainder of the paper, let us fix an input alphabet I and a disjoint output alphabet O, and let us define \(\text {AP}= I \cup O\), \(\Upsilon = \text {{P}}(I)\), \(\Sigma = \text {{P}}(O)\), and \(\Gamma = \text {{P}}(\text {AP})\).
Definition 1
(Labeled Transition System) A finite, \(\Sigma \)-labeled \(\Upsilon \)-transition system is a tuple \(M= (S, s_0, \tau , o)\), where S is nonempty set of states, \(s_0 \in S\) is the initial state, \(\tau : S \times \Upsilon \rightarrow S\) is a transition function, and \(o:S \rightarrow \Sigma \) is a labelling function.
(An LTS word) A word p of a labeled transition system M, is a sequence \((s_0,\upsilon _0, \sigma _0),(s_1,\upsilon _1,\sigma _1),\ldots \) in \((S \times \Upsilon \times \Sigma )^\omega \) such that \(\sigma _i = o(s_i)\) and \(s_{i+1} = \tau (s_i,\upsilon _i)\).
(Path) A path of a word p is the sequence of states induced by p.
(Trace) A trace of a word p is the sequence of input/output pairs induced by p.
We denote by \(\text {traces}\left( M\right) \) the set of all traces of \(M\). The projection of a trace \(\pi \in \text {traces}\left( M\right) \) on \(\Upsilon ^{\omega }\) (resp. \(\Sigma ^\omega \)) is an input (resp. output) trace denoted by \(\upsilon = \mathop {\left( \pi \downharpoonright \Upsilon \right) }\) (resp. \(\sigma = \mathop {\left( \pi \downharpoonright \Sigma \right) }\)). Similarly, for an input trace \(\upsilon \in \Upsilon ^{\omega }\), we denote by \(M(\upsilon )\) the (unique) trace \(\pi \in \text {traces}\left( M\right) \) s. t. \(\upsilon = \mathop {\left( \pi \downharpoonright \Upsilon \right) }\).
(Parallel Composition) Given input trace \(\upsilon \in \Upsilon ^\omega \) and output trace \(\sigma \in \Sigma ^\omega \), their parallel composition denoted by \(\left( \upsilon ~\Vert ~\sigma \right) \) is an infinite word \(\omega = \upsilon _0 \cup \sigma _0, \upsilon _1 \cup \sigma _1,\dots \) over \(\Gamma \).
Temporal logic
Throughout the paper, we denote by \(\varphi \) an LTL formula in negation normal form (NNF), over the set \(\text {AP}\) of atomic propositions [16]. The semantics of LTL is defined over \(\text {AP}\) with respect to infinite paths of \(M\) in a standard way. In this paper, we synthesize systems that satisfy the following simple fragment of CTL\(^*\):
$$\begin{aligned} \Phi {:}{:}{=} \text {{A}}\varphi ~\vert ~ \text {{E}}\varphi ~\vert ~ \Phi \wedge \Phi , \end{aligned}$$
where \(\varphi \) is an LTL formula. The semantics of the universal and existential quantifiers over LTL formulas are defined as expected:
So far we denoted by \(\text {traces}\left( M\right) \) the set of traces of M, where a trace corresponds to a run, which in itself must start from an initial state of M (see Definition 2 and 4). We similarly use \(\text {traces}\left( M,s\right) \) to refer to runs that begin at an arbitrary state \(s\in S\) of M.
For a state s of a transition system \(M\),
$$\begin{aligned} s \models \text {{A}}\varphi&\quad \textit{iff} \quad \forall t \in \text {traces}\left( M,s\right) .~t \models \varphi \;,\\ s \models \text {{E}}\varphi&\quad \textit{iff} \quad \exists t \in \text {traces}\left( M,s\right) .~t \models \varphi \;. \end{aligned}$$
A transition system \(M\) satisfies a formula \(\varphi \), written \(M\models \varphi \), if all its initial states do.
Nondeterministic Büchi automata
An LTL formula can be represented by a nondeterministic Büchi automaton [19]: a tuple \(\mathcal {A}=(Q, q_0, \rho , \alpha )\), where Q is a finite set of states, \(q_0 \in Q\) is the initial state, \(\rho : Q \times \Upsilon \times \Sigma \rightarrow \text {{P}}(Q)\) is the transition relation, and \(\alpha \) is the set of accepting states; recall \(\Sigma \) and \(\Upsilon \) are defined in Sect. 2.1.
(Run of a Büchi automaton) Given an infinite word \(\omega = \upsilon _0\cup \sigma _0,\upsilon _1\cup \sigma _1,\dots \) over \(\Gamma \), The corresponding runs of a Büchi automaton \(\mathcal {A}\), denoted by \(\text {run}\left( w\right) \), are the infinite paths \(\pi =q_0,q_1, \dots \in Q^{\omega }\) where for all \(i \ge 0\), \(q_{i+1} \in \rho (q_i,\upsilon ^i,\sigma ^i)\).
(Accepting run) An accepting run of \(\mathcal {A}\) is a run that visits some accepting state infinitely often; a trace is accepted by \(\mathcal {A}\) if it has a corresponding accepting run, and the language of \(\mathcal {A}\) is the set of all accepted traces.
From this point forward, we denote by \(\mathcal {A}_\varphi \) the nondeterministic Büchi automata that accepts exactly the traces that satisfy \(\varphi \).
Vacuity detection
Informally speaking, a transition system \(M\) satisfies a property \(\varphi \) vacuously if not all parts of \(\varphi \) are instrumental for the satisfaction of \(\varphi \) in \(M\) (in other words, \(M\) satisfies \(\varphi \) in an uninteresting way). As proved in [14], it is sufficient to check vacuity with respect to atomic propositions of \(\varphi \), which, in case of an atomic proposition p appearing in \(\varphi \) in a pure polarity, amounts to model-checking \(\varphi [p \leftarrow \bot ]\), that is, \(\varphi \) where p is replaced with its bottom value.
Hence, we use the following definition of vacuity that allows for efficient detection algorithm:
(Vacuity [2, 14]) A transition system \(M\) satisfies an LTL property \(\varphi \) vacuously iff \(M\models \varphi \) and there exists a literal \(\psi \) of \(\varphi \) which is of pure polarity and \( M\models \varphi [\psi \leftarrow \bot ]\).
The formula \(\varphi [\psi \leftarrow \bot ]\) is a strengthening of \(\varphi \) since \(\varphi [\psi \leftarrow \bot ] \implies \varphi \) and we call the negation \(\varphi _\psi = \lnot {\varphi [\psi \leftarrow \bot ]}\) of a strengthening a witness formula. A trace \(\pi \) of \(M\) that satisfies \(\varphi _\psi \) is called an interesting witness for \(\psi \), since it demonstrates that \(\psi \) is instrumental to the satisfaction of \(\varphi \) in \(M\); \(\pi \) is an interesting witness of \(M\) if it is an interesting witness for some subformula \(\psi \) of \(\varphi \). We note that if \(M\models \bigwedge _i \varphi _i\) then \(M\not \models \bigvee _i\varphi _i[\psi \leftarrow \bot ]\) is relevant to check only for those \(\varphi _i\) in which \(\psi \) appears.
The concept of witnesses and strengthenings is not restricted to Definition 9, and it lends itself, in theory, to other definitions of vacuity [1, 7, 8]. The framework proposed in this paper is orthogonal to the particular definition of vacuity, as long as the strengthenings are \(\omega \)-regular.
Bounded synthesis
Bounded synthesis is a method to construct a finite-state labeled transition system that not only satisfies a given temporal specification \(\varphi \), but also fulfills a constraint on its size [10]. The idea is to let an SMT solver synthesize a transition system M (i.e., choose the transitions and the labeling of the states), such that \(M \times \mathcal {A}_{\lnot \varphi }\) has an empty language.
The synchronous product \(\mathcal {G}\) of a transition system \(M= (S, s_0, \tau , o)\) and a Büchi automaton \(\mathcal {A}_{\lnot \varphi }=(Q, q_0, \rho , \alpha )\) is called the run graph of \(\mathcal {A}_{\lnot \varphi }\) on \(M\).Footnote 4 The states of \(\mathcal {G}\) are annotated with two functions: a reachability function \(\lambda ^\mathbb {B}: Q \times S \rightarrow \mathbb {B}\) and a ranking function \(\lambda ^\#: Q \times S \rightarrow C\subset \mathbb {N}\), where \(C = \{0, \dots , |Q|\times |S|-1\}\). Annotations of \(\mathcal {G}\) (i. e., \(\lambda ^\#\) and \(\lambda ^\mathbb {B}\) functions) are valid if they satisfy the following constraints. First, the initial state is reachable:
$$\begin{aligned} \lambda ^\mathbb {B}(q_0,s_0)\;. \end{aligned}$$
Second, the reachability predicate and the transition system are compatible:
$$\begin{aligned} \bigwedge _{ \begin{array}{c} q ,q' \in Q\\ s,s' \in S\\ \upsilon \in \Upsilon \end{array} } \lambda ^\mathbb {B}(q,s) \wedge q' \in \rho (q, o(s), \upsilon ) \wedge s' \in \tau (s, \upsilon ) \rightarrow \lambda ^\mathbb {B}(q',s')\;. \end{aligned}$$
Finally, the ranking function guarantees that the constraint is satisfiable only if the language of the run graph is empty: For accepting states, we require that the labelling on the target state is strictly larger than on the source (accepting) state:
$$\begin{aligned} \bigwedge _{ \begin{array}{c} q \in \alpha ,q' \in Q\\ s,s' \in S\\ \upsilon \in \Upsilon \end{array} } \lambda ^\mathbb {B}(q,s) \wedge q' \in \rho (q, o(s), \upsilon ) \wedge s' \in \tau (s, \upsilon ) \rightarrow \lambda ^\#(q',s') > \lambda ^\#(q,s)\; \text {;} \end{aligned}$$
and for non-accepting states the labelling on the target states is larger or equal than on the source state:
$$\begin{aligned} \bigwedge _{ \begin{array}{c} q \in Q \setminus \alpha ,q' \in Q\\ s,s' \in S\\ \upsilon \in \Upsilon \end{array} } \lambda ^\mathbb {B}(q,s) \wedge q' \in \rho (q, o(s), \upsilon ) \wedge s' \in \tau (s, \upsilon ) \rightarrow \lambda ^\#(q',s') \ge \lambda ^\#(q,s) \;. \end{aligned}$$
The intuition behind the ranking function is as follows: if the language is not empty, then there is an accepting path (i.e., a lasso-shaped path in the product automaton that includes an accepting state), and then it is impossible to satisfy these constraints over that path. This is because the ranks of states on the cycle cannot be strictly descending. The two automata in Fig. 2 illustrate this point—see caption. Hence, (5)–(8) are satisfiable if and only if the language of the product automaton is empty. The correctness of this construction was proven in [10].
We can assign a number to each state on the left automaton, that satisfies the inequality constraints, e.g., the 0/1 values labeling the states. Such a labeling is impossible for the automaton on the right, because it has an accepting state in a loop
Theorem 1
(Finkbeiner et al. [10]) Given a Büchi automaton \(\mathcal {A}=(Q, q_0, \rho , \alpha )\) constructed from \(\lnot \varphi \), transition system \(M=(S, s_0, \tau , o)\) satisfies \(\text {{A}}\varphi \) iff it corresponds to a solution to the constraints (5)–(8).
Initially, the LTL specification \(\varphi \) is negated and translated to a Büchi automaton \(\mathcal {A}_{\lnot \varphi }\). In the next step, (5)–(8) are solved with an SMT solver based on \(\mathcal {A}_{\lnot \varphi }\). Being unknown, \(\tau \), \(\lambda ^\mathbb {B}\), \(\lambda ^\#\) and o (the labeling function) are represented by uninterpreted functions; thus, the quest for finding \(M\) is reduced to the problem of satisfiability modulo finite integer arithmetic with uninterpreted functions, which is an NP-complete problem.
Non-vacuous bounded synthesis
In this section we describe non-vacuous bounded synthesis—our method for constructing a finite-state labeled transition system that fulfils a constraint on its size and satisfies a given temporal specification non-vacuously.
A specification for non-vacuous satisfaction
A specification \(\varphi \) is satisfied non-vacuously in \(M\) if and only if \(M\) contains a witness for each strengthening of \(\varphi \). In other words, as we stated earlier in (2),
$$\begin{aligned} M\models \text {{A}}\varphi \wedge \bigwedge _{\psi \in \text {Lit}\left( \varphi \right) } \text {{E}}\lnot \varphi [\psi \leftarrow \bot ] \end{aligned}$$
(note that (9) is based on our choice of definition for vacuity—see 9). We call \(\varphi _\psi = \lnot \varphi [\psi \leftarrow \bot ]\) the witness formulas for non-vacuity of \(\varphi \) with respect to \(\psi \).
Note that not all witness formulas add usable information. For instance, for \(\varphi \) as defined in (3), the witness formula \(\varphi _{g_1}\) (i. e., \(\lnot \varphi _1[g_1 \leftarrow \bot ] = \text {{F}}r_1\)) is clearly satisfied by a trace of any system, and the same holds for any satisfiable witness formula that contains only input signals.
We continue in the next subsection by showing how existentially-quantified formulas can be synthesized. Then, we can use this technique to synthesise formulas of the form defined in (9).
Bounded synthesis for existential formulas
Our goal is to synthesize a finite-state labeled transition system with a bound on its size, in which there exists an execution path that satisfies a given temporal specification \(\varphi \). We will define a set of constraints that is different than the case described in Sect. 2.5 to achieve this. Initially, we translate \(\varphi \) to a nondeterministic Büchi automaton \(\mathcal {A}_\varphi \) and create the run graph \(\mathcal {G}\) of \(\mathcal {A}_\varphi \) on \(M\). Then, we use a Boolean marking function \(\lambda ^\mathbb {*}:Q \times S \rightarrow \mathbb {B}\) to indicate that a state is on our selected path in \(\mathcal {G}\). On that selected path, we impose a ranking function that can only be satisfied if it corresponds to an accepting run.
First, the initial state is marked:
$$\begin{aligned} \lambda ^\mathbb {*}(q_0,s_0)\;. \end{aligned}$$
Next, if a non-accepting state is marked, then at least one of its successors is marked, and the ranking of the destination state is strictly smaller:
$$\begin{aligned} \bigwedge _{ \begin{array}{c} q \in Q \setminus \alpha \\ s \in S\\ \upsilon \in \Upsilon \end{array} } \left( \lambda ^\mathbb {*}(q,s) \rightarrow \bigvee _{ \begin{array}{c} q' \in Q\\ s' \in S \end{array} } \left( \begin{array}{l} q' \in \rho (q, o(s), \upsilon ) \wedge s' \in \tau (s, \upsilon ) \wedge \\ \quad \lambda ^\mathbb {*}(q',s') \wedge \lambda ^\#(q',s') < \lambda ^\#(q,s) \end{array} \right) \right) \;. \end{aligned}$$
On the other hand if an accepting state is marked, then we only require that one of its successors is marked (but in contrast to the previous case, here there is no restriction on the ranking of its successor):
$$\begin{aligned} \bigwedge _{ \begin{array}{c} q \in \alpha \\ s \in S\\ \upsilon \in \Upsilon \end{array} } \left( \lambda ^\mathbb {*}(q,s) \rightarrow \bigvee _{ \begin{array}{c} q' \in Q\\ s' \in S \end{array} }\left( \begin{array}{l} q' \in \rho (q, o(s), \upsilon ) \wedge s' \in \tau (s, \upsilon ) \wedge \\ \quad \lambda ^\mathbb {*}(q',s') \end{array} \right) \right) \;. \end{aligned}$$
The two automata in Fig. 3 illustrate our construction—see caption. The following theorem states that these constraints are correct.
On the left there is no accepting run, and indeed there is no ranking function that can satisfy the constraints. On the right there is an accepting run (the \(\lambda ^\mathbb {*}\) predicate is marked with '*'), and the fact that there is no constraint on the outgoing edge of the accepting state allows to find a ranking function, namely the numbers 0,1,2,3,4,5 that are marked inside the states
Given a Büchi automaton \(\mathcal {A}=(Q, q_0, \rho , \alpha )\) constructed from a formula \(\varphi '\), a transition system \(M=(S, s_0, \tau , o)\) satisfies \(\text {{E}}\varphi '\) iff it corresponds to a solution to constraints (10)–(12).
\((\Rightarrow )\) There is a unique run graph \(\mathcal {G}=(G,E)\) for \(\mathcal {A}\) on \(M\). Assume \(M\) is accepted by \(\mathcal {A}\); therefore, \(\mathcal {G}\) contains at least one lasso-shaped path \(\pi = (q_0,s_0)(q_1,s_1) \dots [(q_n,s_n)\dots (q_m,s_m)]^\omega \) such that \(q_i\) is accepting for some \(i\in [n,m]\). We have to show that in such a case (10)-(12) are satisfiable. Marking all the states on the path clearly satisfies (10), and the \(\lambda ^\mathbb {*}\) predicate is true along this path as required by constraints (11) and (12). It is left to show that there exists a ranking function that satisfies (11). Indeed the following function, which annotates each state on \(\pi \) by its distance to \(q_i\), is a valid ranking function:
$$\begin{aligned} \lambda ^\#(q_j,s_j) = {\left\{ \begin{array}{ll} i-j &{}\text{ if } j \le i \\ m-j+i-n+1 &{}\text{ if } i < j. \end{array}\right. } \end{aligned}$$
Indeed, \(\lambda ^\#(q_j,s_j)>\lambda ^\#(q_k,s_k)\) for all \(((q_j,s_j)(q_k,s_k))\in \pi \), unless \(j = i\). Recall that only non-accepting states are bound by constraint (11). The figure below demonstrates this ranking for \(n=3,m=6\), and \(i=5\).
\((\Leftarrow )\) Assume that (10)–(12) are satisfiable. The set of marked states must include a lasso-shaped path beginning from the initial state, and the fact that (11) is satisfied means that there exists an accepting state in the loop. Hence the run graph must contain an accepting path. \(\square \)
Finally, synthesising a non-vacuous system—a system that satisfies (2)—amounts to solving the conjunction of the constraints that were described in Sect. 2.5 (for the universal part), and the constraints in Sect. 3.2 for each \(\psi \in \text {Lit}\left( \varphi \right) \) (for the existential part). A separate discrete ranking function is required for \(\varphi \) and each of its witness formulas.
Corollary 1
A finite-state transition system \(M=(S, s_0, \tau , o)\) satisfies a temporal specification in the form of the CTL\({}^*\) fragment defined in (4) iff it corresponds to a solution to constraints (5)–(8) and (10)–(12).
We note that the addition of (10)–(12) to the bounded synthesis formula, does not change the asymptotic complexity of the problem.
Beyond vacuity
In the introduction we argued that non-vacuous systems are preferable to vacuous systems because they are more likely to fulfill the designer's intent. This guarantees that for specifications like \(\varphi = \text {{G}}(r \rightarrow \text {{F}}g)\), there will be at least one path on which \(\text {{G}}\text {{F}}g\) does not hold. Intuitively, this corresponds to the idea that an input r should trigger the output g. However, the definition of vacuity is somewhat too coarse for our purpose. We need a more refined notion, which will enable us to distinguish between non-systems that are non-vacuous. In the following subsection we introduce a partial order between systems realizing a given specification. We consider a system A strictly less vacuous (or, equivalently, more interesting) than another system B if the set of interesting witnesses in A properly contains the set of interesting witnesses in B. For the property above, for example, this corresponds to additional witnesses to \(\lnot \text {{G}}\text {{F}}g\), i.e., additional traces in which g does not occur without first being 'triggered' by r. For some specifications, there exist least vacuous systems, that is, maximal systems in the partial order of vacuity. In Sect. 4.2, however, we show that for some other specifications the partial order gives rise to infinite vacuity chains, i.e., infinite chains of ever less vacuous systems.
In Sect. 4.3 we show that given a system, we can use a variant of bounded synthesis to synthesize a less vacuous one, which naturally leads to a most interesting (least-vacuous) system of a given size, when such a system exists. Finally, in Sect. 4.4, we show that for our running example there exists such a least-vacuous system.
Partial order on non-vacuous systems
Let \(M_1\) and \(M_2\) be transition systems that satisfy \(\varphi \). Given a witness formula \(\varphi _\psi \), we define a relation \(M_1 \preccurlyeq _\psi M_2\) to indicate that \(M_2\) has at least the same set of interesting witnesses according to \(\varphi _\psi \) as \(M_1\). Formally, given a specification \(\varphi \) and a witness formula \(\varphi _\psi \) of \(\varphi \), we define
$$\begin{aligned} M_1 \preccurlyeq _\psi M_2 \text { iff } \forall \upsilon \in \Upsilon ^{\omega }.\ ( M_1(\upsilon ) \models \varphi _\psi ) \rightarrow (M_2(\upsilon ) \models \varphi _\psi ). \end{aligned}$$
We say that \(M_2\) is strictly less vacuous than \(M_1\) if in addition there is at least one input sequence that leads to an interesting witness only in \(M_2\):
$$\begin{aligned} M_1 \prec _\psi M_2 \text { iff } M_1 \preccurlyeq _\psi M_2 \text { and } \exists \upsilon \in \Upsilon ^{\omega }.\ ( M_1(\upsilon ) \not \models \varphi _\psi ) \wedge (M_2(\upsilon ) \models \varphi _\psi ). \end{aligned}$$
If \(M_1 \preccurlyeq _\psi M_2\) and \(M_2 \preccurlyeq _\psi M_1\), we say that \(M_1\) and \(M_2\) are equivalent in the partial order of vacuity with respect to \(\psi \), denoted \(M_1 \equiv _\psi M_2\).
By extending the relation \(\prec _\psi \) to the set of all witness formulas, we can compare two transition systems in terms of vacuity. Let \(\Psi \) be the set of all witness formulas for \(\varphi \). We define the partial order \(\preccurlyeq _\varphi \) as
$$\begin{aligned} M_1 \preccurlyeq _\varphi M_2 \text { iff } \forall \varphi _\psi \in \Psi .\ M_1 \preccurlyeq _\psi M_2\;, \end{aligned}$$
and the strict partial order \(\prec _\varphi \) as
$$\begin{aligned} M_1 \prec _\varphi M_2 \text { iff } M_1 \preccurlyeq _\varphi M_2 \text { and } \exists \varphi _\psi \in \Psi .\ \left( M_1 \prec _\psi M_2 \right) . \end{aligned}$$
In other words, \(M_2\) is at least as non-vacuous as \(M_1\) w.r.t. all possible witnesses and is strictly less vacuous than \(M_1\) w.r.t. at least one witness formula. Similarly to the above, we say that \(M_1\) is equivalent to \(M_2\) in the partial order of vacuity, denoted \(M_1 \equiv _\varphi M_2\), if \(M_1 \preccurlyeq _\varphi M_2\) and \(M_2 \preccurlyeq _\varphi M_1\).
Since there is a finite number of transition systems of any size N, for a given LTL formula \(\varphi \), there exists at least one least vacuous system \(M^\varphi _N\) of size N, according to \(\prec \), assuming that \(\varphi \) is realizable by a system with N states. This system may not be unique. Moreover, if there are several least-vacuous systems of size N, they can be equivalent or incomparable.
It is easier to reason about equivalent and incomparable systems if we re-define the partial order on systems as follows. We can view the above partial order on systems realizing \(\varphi \) as a partial order on subsets of the (infinite) set of all input traces \(\mathcal{V} = \{ \upsilon : \upsilon \in \Upsilon ^\omega \}\). A system \(M\) realizing \(\varphi \) can be mapped to the set of input traces \(V(M,\varphi )\) that induce interesting witness traces in \(M\) with respect to some subformula of \(\varphi \). We can similarly denote by \(V(M,\varphi _\psi )\) the set of input traces that induce interesting witness traces in \(M\) with respect to a particular witness formula \(\varphi _\psi \). Then, it is easy to see that (13) is equivalent to
$$\begin{aligned} M_1 \preccurlyeq _\psi M_2 \text { iff } V(M_1,\varphi _\psi ) \subseteq V(M_2,\varphi _\psi ), \end{aligned}$$
and the strict inequality holds if the set \(V(M_1,\varphi _\psi )\) is a strict subset of \(V(M_2,\varphi _\psi )\). Also, \(M_1 \equiv _\psi M_2\) if \(V(M_1,\varphi _\psi ) = V(M_2,\varphi _\psi )\).
Similarly, (15) can be rewritten as
$$\begin{aligned} M_1 \preccurlyeq _\varphi M_2 \text { iff } \forall \varphi _\psi \in \Psi .\ V(M_1,\varphi _\psi ) \subseteq V(M_2,\varphi _\psi ), \end{aligned}$$
and the strict inequality holds if the set \(V(M_1,\varphi _\psi )\) is a strict subset of \(V(M_2,\varphi _\psi )\) for some \(\varphi _\psi \in \Psi \). Two systems \(M_1\) and \(M_2\) realizing \(\varphi \) are equivalent with respect to \(\varphi \) (i.e., \(M_1 \equiv _\varphi M_2\)) if and only if the following holds:
$$\begin{aligned} \forall \varphi _\psi \in \Psi .\ V(M_1,\varphi _\psi ) = V(M_2,\varphi _\psi ). \end{aligned}$$
Finally, if \(M_1 \not \preccurlyeq _\varphi M_2\) and \(M_2 \not \preccurlyeq _\varphi M_1\), we say that \(M_1\) and \(M_2\) are incomparable.
The following theorem clarifies the difference between incomparable and equivalent least-vacuous systems using (18) and (19).
The following claims hold for any LTL formula \(\varphi \).
If there exists a system \(M_{max}\) realizing \(\varphi \) such that
$$\begin{aligned} \forall \varphi _\psi \in \Psi .\ V(M_{max},\varphi _\psi ) = \bigcup _{M\textit{ realizes } \varphi } V(M,\varphi _\psi ), \end{aligned}$$
then \(M_{max}\) is a least-vacuous system realizing \(\varphi \), and any other least-vacuous system \(M'\) realizing \(\varphi \) is equivalent to \(M_{max}\).
If \(\varphi \) is realizable and there is no system \(M_{max}\) that realizes \(\varphi \) and satisfies (20), then either
there is an infinite vacuity chain; or
there are several incomparable least-vacuous systems.
We prove the claims separately.
If there exists \(M_{max}\) realizing \(\varphi \) such that (20) holds, then by (18), for any other \(M\) realizing \(\varphi \), we have \(M\preccurlyeq _\varphi M_{max}\), hence \(M_{max}\) is a least-vacuous system realizing \(\varphi \). Now assume that there is another system \(M'\) that is a least-vacuous system realizing \(\varphi \). Then,
$$\begin{aligned} \forall \varphi _\psi \in \Psi .\ V(M', \varphi _\psi ) \subseteq \bigcup _{M\textit{ realizes } \varphi } V(M,\varphi _\psi ) \end{aligned}$$
(as \(M'\) is one of the systems in the union), hence \(M' \preccurlyeq _\varphi M_{max}\). Therefore, \(M'\) and \(M_{max}\) are not incomparable. Since \(M'\) is least vacuous, it also holds that \(M'\succeq M_{max}\), and hence they are equivalent in the vacuity preorder.
Assume that there is no system that satisfies (20) and let \(M_1\) be a least-vacuous system realizing \(\varphi \) (if there is no such \(M_1\), then there is an infinite vacuity chain, and the claim holds trivially). In particular, since \(M_1\) does not satisfy (20), we have
$$\begin{aligned} V(M_1, \varphi _\psi ) \subset \bigcup _{M\textit{ realizes } \varphi } V(M,\varphi _\psi ) \end{aligned}$$
for at least one witness formula \(\varphi _\psi \) of \(\varphi \). Consider an input trace
$$\begin{aligned} \upsilon \in \Big ( \bigcup _{M\textit{ realizes } \varphi } V(M,\varphi _\psi ) \Big ) \setminus V(M_1, \varphi _\psi ). \end{aligned}$$
Assume that there exists \(M_2\) realizing \(\varphi \) that contains an interesting witness trace for \(\varphi _\psi \) induced by \(\upsilon \). By construction, \(M_1\) and \(M_2\) are incomparable. Hence, either \(M_2\) is also a least-vacuous system, which is incomparable to \(M_1\) (which concludes the proof), or there exists another system \(M_3\) such that \(M_2 \prec _\varphi M_3\) and \(M_3\) is a least-vacuous system realizing \(\varphi \) (recall that we assumed that there are no infinite vacuity chains). Then, \(M_1\) and \(M_3\) are two incomparable least-vacuous systems realizing \(\varphi \).
The following examples illustrate the notion of least-vacuous systems. Example 1 shows a specification for which there exist two equivalent least-vacuous systems. Example 2 and the example in "Appendix 1" show specifications for which there are two incomparable least-vacuous systems.
[Equivalent least-vacuous systems] Consider the following specification:
$$\begin{aligned} \varphi = \text {{G}}(r \implies \text {{F}}g)\;, \end{aligned}$$
where the sole interesting witness formula is \(\varphi _r = \text {{F}}\text {{G}}(\lnot g)\). Figure 4 demonstrates two systems of size 2 realizing \(\varphi \). It is easy to see that
$$\begin{aligned} V(M_0,\varphi _r) = V(M_1, \varphi _r), \end{aligned}$$
that is, all non-vacuous traces of \(M_0\) are still non-vacuous in \(M_1\) and vice-versa. In other words, \(M_0 \equiv _\varphi M_1\). Yet, the systems are not isomorphic. As an example of the difference between \(M_0\) and \(M_1\), consider the run of \(M_0\) on the input trace \((\lnot r)^\omega \):
$$\begin{aligned} M_0((\lnot r)^\omega ) = \{\lnot r, \lnot g\} ^\omega \;. \end{aligned}$$
On the other hand, the run of \(M_1\) on the same input trace is:
$$\begin{aligned} M_1((\lnot r)^\omega ) = \{\lnot r, g \}, \{\lnot r, \lnot g\} ^\omega \;. \end{aligned}$$
Least-vacuous systems realizing \(\text {{G}}(r\rightarrow \text {{F}}g)\)
Proposition 1
\(M_0\) and \(M_1\) are least-vacuous systems realizing \(\varphi \).
As \(M_0 \equiv _\varphi M_1\), it suffices to prove that \(M_0\) is a least-vacuous system realizing \(\varphi \). Let \(M\) be an arbitrary system that realizes \(\varphi \). For an input sequence \(\upsilon \in \Upsilon ^{\omega }\), assume that \(\upsilon \) induces a path in \(M\) that satisfies \(\varphi _r = \text {{F}}\text {{G}}(\lnot g)\). Since this path, in particular, satisfies \(\varphi \), it also satisfies \(\text {{F}}\text {{G}}( \lnot r)\) (otherwise there would have been requests that are never granted). Observing Fig. 4, it is easy to see that the same input sequence \(\upsilon \) would induce a path in \(M_0\) with an infinite suffix \(\{s_0\}^\omega \), hence, in particular, it satisfies \(\text {{F}}\text {{G}}(\lnot g)\). Hence, \(M\) is not less vacuous than \(M_0\). \(\square \)
The following is an example of two incomparable least-vacuous systems, illustrating the second case in 3(b).
[Incomparable least-vacuous systems] Consider the specification \(\varphi \), which is the conjunction of the following three properties:
$$\begin{aligned} \varphi _1 = r \rightarrow \text {{X}}g_1, \quad \varphi _2 = r \rightarrow \text {{X}}g_2, \quad \varphi _3 = \text {{X}}(g_1 \vee g_2)\;, \end{aligned}$$
where r is an input, and \(g_1\) and \(g_2\) are outputs. The interesting witness formulas for \(\varphi \) are
$$\begin{aligned}\lnot \varphi _1[r\leftarrow \bot ] = \text {{X}}(\lnot g_1),\quad \lnot \varphi _2[r\leftarrow \bot ] = \text {{X}}(\lnot g_2)\;. \end{aligned}$$
In any system that realizes \(\varphi \), satisfying the witness formula \(\text {{X}}(\lnot g_1)\) implies that the second state must be labelled with \(\lnot g_1 \wedge g_2\) if \(\lnot r\) is its input (because of \(\varphi _3\)). At the same time in order to satisfy \(\text {{X}}(\lnot g_2)\) the second state of this system must be labelled with \(g_1\wedge \lnot g_2\), which clearly contradicts the previous requirement.
On the other hand, least-vacuous systems for \(\varphi \) exist. For example, consider the two systems in Fig. 5: the left satisfies \(\text {{E}}\text {{X}}(\lnot g_1)\) and the right satisfies \(\text {{E}}\text {{X}}(\lnot g_2)\), but neither satisfies both. Furthermore, it is not hard to see that both \(M_1\) and \(M_2\) are least-vacuous with respect to \(\varphi \) (the proof would be similar to the proof of Proposition 1).
Both \(M_1\) and \(M_2\) realize \(\varphi \) from (22) least-vacuously, but are incomparable
Infinite vacuity chains
For some formulas, there is an infinite chain of ever less vacuous (and ever larger) systems. As an example, consider the following LTL specification:
$$\begin{aligned} \varphi = (\text {{G}}r) \implies (\text {{F}}g) \;. \end{aligned}$$
The only useful witness formula for \(\varphi \) is
$$\begin{aligned} \varphi _r = \text {{G}}\lnot g\;. \end{aligned}$$
Figure 6 depicts an abstract transition system \(M_k\) of arbitrary size (i. e., \(k+3\)) that realizes specification \(\varphi \) non-vacuously for any k.
An example of infinite vacuity chain
\(\forall k.\ M_k \prec _\psi M_{k+1}\).
We have to show that \(M_{k+1}\) is as non-vacuous as \(M_k\) and that there exists an input trace that makes \(M_{k+1}\) less vacuous w.r.t. \(\varphi _r\).
First we show \(\forall k.\ M_k \preccurlyeq _\psi M_{k+1}\). For each input trace \(\pi \in \Upsilon ^\omega \), if \(M_k(\pi ) \models \text {{G}}\lnot g\), then \(\pi \models r^j(\lnot r)^+(\lnot r + r)^\omega \) for some \(j\le k\), so \(M_{k+1}(\pi ) \models \text {{G}}\lnot g\).
To see that \(\forall k.\ M_k \prec _\psi M_{k+1}\) holds, note that the input trace \(r^{k+1}(\lnot r)^\omega \) leads to an interesting trace in \(M_{k+1}\) but not in \(M_k\). \(\square \)
Synthesizing a less vacuous system
We now discuss how to synthesize a less vacuous system \(M_2\) given a correct system \(M_1\). We do this by expressing the partial order defined above in the simple fragment of CTL\({}^*\)defined in (4).
Given a formula \(\varphi \) or a system M, we use a primed version (\(\varphi '\) or \(M'\), respectively) to denote the formula/system obtained by replacing all output literals by primed versions. Given a system \(M_1\) that satisfies \(\varphi \), we have \(M_1 \prec _\psi M_2\) iff
$$\begin{aligned} M'_1 \times M_2\models \text {{A}}\varphi \wedge \text {{A}}(\varphi '_{\psi } \rightarrow \varphi _\psi ) \wedge \text {{E}}(\lnot \varphi '_{\psi } \wedge \varphi _\psi )\;. \end{aligned}$$
Equation (25) follows directly from Eq. (14) after renaming the variables of \(M_1\) with their primed versions. Note that \(\varphi \) and \(\varphi _\psi \) refer to the outputs of \(M_2\) and \(\varphi '_{\psi }\) refers to the outputs of \(M_1\), while both systems receive the same inputs. The following theorem generalizes (25) to all subformulas of \(\varphi \).
\(M_1\) is strictly less vacuous than \(M_2\) iff
$$\begin{aligned} M'_1 \times M_2 \models \text {{A}}(\varphi \wedge \bigwedge _{\varphi _\psi \in \Psi }( \varphi '_{\psi } \rightarrow \varphi _\psi )) \wedge \text {{E}}(\bigvee _{\varphi _\psi \in \Psi }( \lnot \varphi '_{\psi } \wedge \varphi _\psi ))\;. \end{aligned}$$
Note that this equation has the form of Eq. (2) and can thus be solved as described in Sect. 3.
We iteratively synthesize less and less vacuous systems by applying (26) where \(M_2\) is the existing system. The result is \(M_1'\), which then becomes \(M_2\) of the next iteration. We repeat this process until (26) becomes unrealizable with the current bound on the number of states. We can then either stop or increase the bound. Every such step adds a linear number of variables. Since the asymptotic complexity has an exponential dependence on the number of variables, eventually this formula may become too hard to solve in practice.
A least-vacuous system for the running example
Consider once again our running example from the introduction. Figure 7 shows a least-vacuous system \(M_2\) with the bound 4 on the number of states (one of the intermediate iterations resulted in \(M_1\) depicted in Fig. 7).
The final non-vacuous system \(M_2\)
System \(M_2\) is strictly less vacuous than \(M_1\). Recall that the two witness formulas are \(\varphi _{r_1} = \text {{F}}\text {{G}}\lnot g_1\) and \(\varphi _{r_2} = \text {{F}}\text {{G}}\lnot g_2\). It is not hard to verify that all interesting paths in \(M_1\) w.r.t. to \(\varphi _{r_1}\) (w.r.t. to \(\varphi _{r_2}\)) are also interesting w.r.t. to \(\varphi _{r_1}\) (w.r.t. to \(\varphi _{r_2}\), resp.) in \(M_2\). Also, the trace that results from leaving \(r_1\) and \(r_2\) low all the time is interesting w.r.t. \(\varphi _{r_2}\) in \(M_2\) but not in \(M_1\).
\(M_2\) is a least-vacuous system with respect to \(\{\varphi _{r_1}, \varphi _{r_2}\}\).
Let \(M\) be an arbitrary system that realizes \(\varphi \). For an input sequence \(\upsilon \in \Upsilon ^{\omega }\), assume that \(\upsilon \) induces a path in \(M\) that satisfies \(\varphi _1[r_1 \leftarrow \bot ] = \text {{F}}\text {{G}}\lnot g_1\). Since this path, in particular, satisfies \(\varphi \), it also satisfies \(\text {{F}}\text {{G}}\lnot r_1\) (otherwise there would have been requests that are never granted). Observing Fig. 7, it is easy to see that the same input sequence \(\upsilon \) would induce a path in \(M_2\) with an infinite suffix \({\{s_0,s_2\}}^\omega \), hence, in particular, it satisfies \(\text {{F}}\text {{G}}\lnot g_1\). A similar argument holds for \(\varphi _2[r_2 \leftarrow \bot ]\). Hence, \(M\) is not less vacuous than \(M_2\). \(\square \)
The question whether a given system is a least-vacuous one (again, such systems may not be unique) is equivalent to asking whether a less vacuous one exists, which, by (26) can be reduced to a CTL\({}^*\)realizability question.
Experimental evaluation
We implemented the described technique in the PARTY synthesizer [13]. We cannot check directly whether non-vacuous synthesis leads to a system which is closer to 'the user intent'. However, we can check something with a similar flavor: the ability of this technique to guess missing parts of a specification. Hence, we conducted the following experiment: first, we synthesized models for three complete and correct specifications; then, we made them incomplete by removing some of the conjuncts in the specification; finally, we ran non-vacuous synthesis on these incomplete specifications, and checked whether the resulting system satisfies the original, complete specification; A positive answer indicates that non-vacuous synthesis can accelerate the convergence towards the desired system.
Indeed, in the three experiments that we conducted, non-vacuous synthesis was able to synthesize a system that satisfies the original, full specification, although we emphasize that this is not guaranteed in general. The synthesized system in all three cases is not identical to the one synthesized according to the full specification, which reflects the fact that many systems can satisfy the same specification. It is up to the user to choose between them.
More details about the experimental setting, as well as a performance comparison, is given in 1. It is evident from the comparison that, as expected, on average non-vacuous bounded synthesis takes more time than bounded synthesis.
A 'next' arbiter
The 'next' arbiter of two clients issues a grant for each client in the next step if and only if the client sends a request. The assumption is that clients never send requests simultaneously; thus, issued grants should be mutually exclusive. The complete and incomplete specification of this arbiter for two clients is shown in Fig. 8. The specification should be interpreted as 'every run that satisfies the \(\text {{assume}}\) predicates should also satisfy the \(\text {{guarantee}}\) predicates'.
LTL specification for the 'next' arbiter of two clients. Note that the incomplete specification excludes the right-to-left implications in the guarantee
As depicted in Fig. 9a, b, even a slight modification in the specification results in a large gap in the behaviors of the synthesized systems. On the other hand starting from the system depicted in Fig. 9b, three iterations of the non-vacuous synthesis process result in the system shown in Fig. 9c, which satisfies the original, full specification. Figure 10 depicts the runtime breakdown of bounded synthesis and non-vacuous bounded synthesis for both the complete and incomplete versions of the 'next' arbiter.
Synthesized arbiters of the complete and incomplete specifications of the 'next' arbiter that appeared in Fig. 8
Runtime breakdown of synthesis of the 'next' arbiter
A 'full' arbiter
A 'full' arbiter of two clients eventually issues a grant for each client if the client sends a request. The complete specification appears in Fig. 11 (left), and a partial specification appears in Fig. 11 (right). The properties that are removed in the partial specification state that grants are never given "unnecessarily".
LTL specification for 'full' arbiter of 2 clients
The transition systems that are synthesized for the full and partial specification appear in Fig. 12a, b respectively. On the other hand, starting from the partial specification, after four iterations of the non-vacuous synthesis the system we get is as shown in Fig. 12c, which again satisfies the full specification. Figure 10 depicts the runtime breakdown of bounded synthesis and non-vacuous bounded synthesis for both the complete and incomplete versions of the 'full' arbiter (Fig. 13).
Synthesized arbiters of complete and incomplete specifications of full arbiter as read in Fig. 11
Runtime breakdown of synthesis of the 'full' arbiter
A 'Pnueli' arbiter
A 'Pnueli' arbiter of two clients is a handshake mechanism such that whenever a client sets a request the arbiter will set and keep the corresponding grant high as long as the request is high [12]. The complete and incomplete specification of a 'Pnueli' arbiter of two clients is shown in Fig. 14. The incomplete specification allows the arbiter to set a grant and never unset it; therefore, the synthesized system may issue vacuous grants for each client infinitely often unless the other client sends a request—see Fig. 15b.
LTL specification for a 'Pnueli' arbiter of two clients. The incomplete specification lacks the right-to-left implication in the 4th and 5th lines of the guarantee
The result of our non-vacuous synthesis from the partial specification again satisfies the full specification, as shown in Fig. 15c, and is synthesized in one step. This system also satisfies the specification in a less vacuous way than the system synthesized from the complete specification using the previous version of PARTY, without the new functionality of non-vacuity. Figure 10 depicts runtime breakdown of both synthesis methods for complete and incomplete versions of the 'Pneuli' arbiter (Fig. 16).
Synthesized arbiters of complete and incomplete specifications of a 'Pnueli' arbiter as read in Fig. 14
Runtime breakdown of synthesis of the 'Pnueli' arbiter
In synthesis, it is hard to expect the designer to think of a complete specification. As a result, the large range of possible systems that satisfy the specification permits designs that stand in contrast to the designer's intent. We proposed in this article to apply the concept of vacuity to address this problem. Our method narrows down the range of legitimate synthesised system to those that satisfy the (partial) specification in a meaningful way, a well-known concept from using vacuity in model-checking. But as we argued, we do not have to commit to the Boolean nature of the classical definition of vacuity: we showed how a system can be made less vacuous, even if it already satisfies the specification non-vacuously. Our experiments showed that our method is capable of synthesising better designs, in the sense that they even satisfy parts of the specification that we deliberately removed and were hence inaccessible to the synthesis algorithm. Perhaps in the future synthesis will be used in the industry, and then our conjecture that this process can save time to the designer will be tested with a user-study.
Our solution is based on a novel bounded synthesis technique that combines universal and existential properties; It paves the way for generalizing our technique to full CTL\(^*\). Our tool PARTY is available on the web to try and improve.
This means that we swap \(\psi \) with falseif \(\psi \) is in positive polarity, and with trueotherwise. Hence, e.g., if \(\varphi \equiv \psi _1 \Rightarrow \Psi _2\), then \(\varphi [\psi _1 \leftarrow \bot ] \equiv \psi _2\).
https://extgit.iaik.tugraz.at/scos/scos.sources/party-eris.
Note that these are Moore machines. As such the output of a transition leaving a state appears in the state itself. Hence, for example, in the trace \(\{g_2, r_1\}, \{g_1,r_1,r_2\},\{g_2\}^{\omega }\), the request \(r_1\) on the outgoing edge of \(s_1\) is granted by the label \(g_1\) in \(s_1\).
Since \(\mathcal {G}\) is only used for checking emptiness, the labels are immaterial, and it is customary to use a one-letter automaton (i. e., \(\vert \Sigma \vert = \vert \Upsilon \vert = 1\)).
Armoni R, Fix L, Flaisher A, Grumberg O, Piterman N, Tiemeyer A, Vardi MY (2003) Enhanced vacuity detection in linear temporal logic. In: CAV, LNCS, Springer, vol 2725, pp 368–380
Beer I, Ben-David S, Eisner C, Rodeh Y (2001) Efficient detection of vacuity in ACTL formulas. Formal Methods Syst Des 18(2):279–290
Bloem R, Chatterjee K, Greimel K, Henzinger TA, Hofferek G, Jobstmann B, Könighofer B, Könighofer R (2014) Synthesizing robust systems. Acta Inf 51:193–220
MathSciNet Article Google Scholar
Bloem R, Chatterjee K, Henzinger TA, Jobstmann B (2009) Better quality in synthesis through quantitative objectives. In: CAV, LNCS, Springer, vol 5643, pp 140–156
Bloem R, Chockler H, Ebrahimi M, Strichman O (2017) Synthesizing non-vacuous systems. In: Proceedings of the 18th international conference in verification, model checking, and abstract interpretation (VMCAI), Lecture notes in computer science, Springer, vol 10145, pp 55–72
Bustan D, Flaisher A, Grumberg O, Kupferman O, Vardi M (2005) Regular vacuity. In: CHARME, LNCS, Springer, vol 3725, pp 191–206
Chechik M, Gurfinkel A (2004) Extending extended vacuity. In: FMCAD, LNCS, vol 3312
Chockler H, Gurfinkel A, Strichman O (2013) Beyond vacuity: towards the strongest passing formula. Formal Methods Syst Des 43(3):1–8
Church A (1963) Logic, arithmetics, and automata. In: ICM, institut Mittag-Leffler, pp 23–35
Finkbeiner B, Schewe S (2012) Bounded synthesis. Int J Softw Tools Technol Transf 15(5):519–539
MATH Google Scholar
Jacobs S, Bloem R, Brenguier R, Könighofer R, Pérez GA, Raskin J, Ryzhyk L, Sankur O, Seidl M, Tentrup L, Walker A (2015) The second reactive synthesis competition. In: SYNT
Jobstmann B, Staber S, Griesmayer A, Bloem R (2012) Finding and fixing faults. J Comput Syst Sci 78(2):35–49
Khalimov A, Jacobs S, Bloem R (2013) PARTY parameterized synthesis of token rings. In: CAV, pp 928–933
Kupferman O, Vardi M (2003) Vacuity detection in temporal model checking. J Softw Tools Technol Transf 4(2):224–233
Namjoshi KS (2004) An efficiently checkable, proof-based formulation of vacuity in model checking. In: CAV, LNCS, Springer, vol 3114, pp 57–69
Pnueli A (1977) The temporal logic of programs. In: FOCS, pp 46–57
Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: POPL, Austin, pp 179–190
Samanta R, Deshmukh JV, Chaudhuri S (2013) Robustness analysis of networked systems. In: VMCAI, pp 229–247
Vardi M, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1–37
We would like to thank Nir Piterman for his insights on infinite chains of ever less vacuous systems and Ayrat Khalimov for his comments on existential bounded synthesis and his valuable assistance with the implementation.
Open access funding provided by Graz University of Technology.
Graz University of Technology, Graz, Austria
Roderick Bloem & Masoud Ebrahimi
King's College London, London, UK
Hana Chockler
Information Systems Engineering, IE, Technion, Haifa, Israel
Ofer Strichman
Roderick Bloem
Masoud Ebrahimi
Correspondence to Ofer Strichman.
This work was supported by the Austrian Research Promotion Agency (FFG) through project TRUSTED (867558), Graz University of Technology's LEAD project "Dependable Internet of Things in Adverse Environments".
A: An example of incomparable least-vacuous systems
Consider the specification \(\varphi \) that is a conjunction of the following four properties:
$$\begin{aligned} \varphi _1&= \text {{G}}(r_1 \rightarrow \text {{F}}g_1)\;, \quad \varphi _2 = \text {{G}}( \lnot g_1 \rightarrow \text {{X}}g_2)\;, \\ \varphi _3&= \text {{G}}(r_2 \rightarrow \text {{F}}g_2)\;, \quad \varphi _4 = \text {{G}}( \lnot g_2 \rightarrow \text {{X}}g_1) \;, \end{aligned}$$
where \(r_i\) is an input and \(g_i\) is an output. The following interesting witness formulas
$$\begin{aligned} \lnot \varphi _{1}[r_1 \leftarrow \bot ] = \text {{F}}\text {{G}}(\lnot g_1)\;,\\ \lnot \varphi _{3}[r_2 \leftarrow \bot ] = \text {{F}}\text {{G}}(\lnot g_2)\;. \end{aligned}$$
give rise to incomparable least-vacuous systems as described in Fig. 17. Indeed, the witness formula \(\text {{F}}\text {{G}}(\lnot g_1)\) (resp. \(\text {{F}}\text {{G}}(\lnot g_2)\)) requires a trace that satisfies it to have a suffix \(\lnot g_1^\omega \) (resp. \(\lnot g_2^\omega \)), hence in order to satisfy the property \(\varphi _2\) (resp. \(\varphi _4\)), the same suffix should satisfy \(\text {{X}}(g_2^\omega )\) (resp. \(\text {{X}}(g_1^\omega )\)). Thus, each trace either satisfies the interesting witness \(\text {{F}}\text {{G}}(\lnot g_1)\) or \(\text {{F}}\text {{G}}(\lnot g_2)\), but not both, hence only one of the two sets of witness traces can be maximized. The proof of the least vacuity is similar to the proofs of Propositions 1 and 3.
Incomparable least-vacuous systems realizing \(\varphi \)
B: Performance comparison
Here we compare the performance of non-vacuous bounded synthesis to 'normal' bounded synthesis, using a benchmark set of 164 specifications. The set includes the LTL-Real benchmarks of synthcomp 2020, lily, genbuf, acacia+, and party-elli. Our implementation uses Z3 4.8.10 and SPOT 2.9. It is worth mentioning that our implementation uses integer encoding of co-büchi automata for both methods.
We ran each experiment twice and each time for a total of 60 minutes. In both runs, 70 experiments timed out, 85 were realizable, and 9 were unrealizable. We averaged the run-time profile of both runs and computed the performance loss in making the synthesis non-vacuous.
Of all realizable experiments the non-vacuous bounded synthesis gained negligible performance in three cases. Meanwhile, non-vacuous bounded synthesis timed out on 3 experiments that were realizable through bounded synthesis. Table 1 gives a more detailed comparison.
Table 1 Performance comparison
The biggest factor in the performance loss is the solver time. This is evident in the plots shown in Figs. 18 and 19. Other than the solver time, much of the run-time is spent on translating each specification to a co-büchi automaton, which is shared by both synthesis methods; thus, the total performance loss is typically less than the solver performance loss.
Performance loss on total synthesis time
Performance loss on solver time
Open Access This 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/.
Bloem, R., Chockler, H., Ebrahimi, M. et al. Vacuity in synthesis. Form Methods Syst Des 57, 473–495 (2021). https://doi.org/10.1007/s10703-021-00381-5
Accepted: 11 August 2021
Issue Date: September 2021
Reactive synthesis
Vacuity
Over 10 million scientific documents at your fingertips
Switch Edition
Academic Edition
Manage cookies/Do not sell my data
Not affiliated
© 2022 Springer Nature Switzerland AG. Part of Springer Nature.


Had a nice talk with my dad. I mentioned mom always said time was passing quickly. I said I felt it. It is relentless. I kidded and said' even my allergies take a day off.' He said this feeling is delicate and should be valued. There are internal feelings to be worked out. They are private and individual. He said he thought life had three phases, and at 63 I'm beginning the third phase. He said my work reflects the inner workings we're talking about. They are not negative, but rich with experience. He felt mom was present when we talk about such things. Her wisdom is there. These inner workings should not be denied.
Ah yes, all the private moments. I mentioned to him sometimes they are painful, they are unknown. He said no need to run from them.
I also mentioned if I was younger my art and writing would be about external experience. Now the concern is with the internal. There was a nice softness in his voice.
I said so many tie-ins, resolutions, we don't get to complete. We just get a slice of what can be done. He said this indicates depth in my thinking. He said that's okay, enough is completed and covered to make a difference (my words).


text:
PHOTOS: Migal Vanas
INTERVIEW: Jasmine Perrier
For those who are new to your music, could you introduce yourself?
My name is Oshri (26), I'm a French Yemeni singer based in Los Angeles, an optimistic person and a Spice Girls fan.
How did you first get involved in the music world?
I first started by annoying my whole family and singing all the time, anywhere and everywhere. They told me to shut up so I decided to make a career out of it and joined a boys band when I was 14. The band was a success and from there, there was no turning back.
Your music career took off when you won the first ever South African TRACE Music Stars competition. What can you tell us about this experience?
It was the pilot of the show so I didn't know anything about it. I didn't have cable so I wasn't familiar with the channel and I didn't know who Wyclef Jean was. All I had was a brochure my friend sent me saying you can call, sing and win something. The first audition was literally on the phone, then they went through the thousands of calls and invited people to the real audition, and from there to the actual TV show. It was fun, I never really won anything before. The part that I will never forget and I think was the part that changed my life was the conversations I had with Wyclef after I won, he showered me with compliments and encouragement and told me I had to come to New York to work with him.
Then you moved to America and you first signed to Akon's label before starting releasing music as an independent artist. What has changed for you since you decided to keep moving forward on your own as an artist?
Being signed to Akon had a lot of benefits and it opened a lot of doors for me, but then it was time to take things to the next level, and I needed my freedom to do so.
How would you personally describe yourself as artist and your music style? Would you say that your cultural roots have influenced your sound somehow?
Let's say that if Enrique Iglesias, Michael Jackson and George Michael had a baby, in the Middle East, that would be me. Growing up, my mom always used to play a lot of Middle Eastern music and you hear it in the way I sing today. My jam was pop on MTV so the mix between the two is pretty much what I'm doing today.
Was it challenging to find yourself sonically and lyrically?
Oh yes, and I'm still searching. It's a never-ending process. I have a few dominant layers in my personality so you can literally divide my song collection accordingly.
You released last month your track ''Genie in a Bottle''. Could you tell us about a bit about how it came to life?
Well, you know it's a 90s cover originally done by Christina Aguilera. I played my version of the song in my love shoes in LA and the crowd really liked it so we decided to put it out…
What can we expect from your upcoming sounds and music work?
I just dropped a new original song called "Right Now" which is a collaboration I did with my boy Max Stark, produced by Phynx. We had a late night session on a Saturday, we started jamming and this song came to life. It was one of those sessions that you didn't care about, we were just there for the love of music and of course when you're not trying, then the best things happen.
What effect do you want your work as an artist to have on people?
As an artist, I'd like to promote self love and acceptance. Insecurity is the biggest disease of our generation and it's effecting everything you do. When you love yourself, with your imperfections, then you'll be able to love others, and by loving others you'll be able to contribute and give back to the world. With my sound, I'd like people to feel free, feel sexy, feel empowered and really just connect with the different parts of their emotions.
What has been the biggest lesson you have learned since you started music?
The biggest thing I've learned and I am still working on is letting go of control. You can plan and strategize, but you never know what's really going to happen so you would rather not be attached to the end result and enjoy the process while you can. Patience is another thing I'm still trying to learn.
How do you envision the rest of your journey in the music world?
Have you seen Bohemian Rhapsody? So pretty much like that, just with a happy ending.
Would you have any goals you'd like to accomplish in the near future, or specifically in 2019?
I have 4 EPs I'm planning to drop this year, and I am working on building a new team in the US. If I get both done, I'll be happy! Oh, a breakout song can also be nice.
How do you see the music industry changing? In what direction would you like it to shift?
At the moment no one knows what's coming up next, so things are open and people are open to new things. I'm going to bring the Middle Eastern sound to the front of pop music, slowly but surely.
Do you have a quote, mantra, or philosophy you live by?
Yes, "the purpose of life is to find your gift, the meaning of life is to give it away" —Picasso.
We are coming to an end. Is there anything else you would like us to know or any special message you would like to add?
What keeps me going is my internal engine of happiness and belief. So no matter who you are and what you're trying to achieve, make sure to work on yourself from the inside, and don't stop until you get everything you truly desire from this world.
CONNECT WITH OSHRI: WEBSITE | TWITTER | FACEBOOK | INSTAGRAM | YOUTUBE
Categories FEATURES, MUSIC
Previous Grace Van Dien | ISSUE NO.13
Next Get to know VillageOne, an innovative co-working space for creatives in New York

redpajama_set_name: RedPajamaCommonCrawl


St James's Gate. View across vathouse rooftops, Market Street.
The quarter will be a mixed use area with commercial, office and residential space and will be fully integrated into the wider Liberties area.
INTERNATIONAL DRINKS GIANT Diageo has announced plans to develop an urban quarter at the site of the Guinness brewery in Dublin.
Diageo – which produces Guinness – plans to develop 12.6 acres at St James's Gate into "one of the most dynamic urban quarters in Ireland and Europe".
The multinational drinks company said advancements in technology and significant investment meant that it could now brew more beer with less space at the historic brewery.
As a result of this it will transform 12.6 acres of the nearly 50 acre St James's Gate site, which has been a mainstay of the Dublin city brewing landscape for hundreds of years.
According to Diageo, the new urban development will be called the St James's Gate Quarter.
Diageo said that it had worked with planning and architectural experts to create a vision that is underpinned by the Dublin City Development Plan and the Liberties Local Area Plan (where the site is located).
The quarter will be a mixed use area with commercial, office and residential space and will be fully integrated into the wider Liberties area. Diageo said there will also be public spaces and streets within the quarter.
It said it is now searching for a development partner to help it create the quarter.
The development will be phased over a long period, and Diageo said it will retain ownership of the iconic St James's Gate and Arthur Guinness's residence.
"We are committed to a long-term sustainable future at St James's Gate and are delighted to be opening streets, creating spaces, and generating opportunity," said country director for Diageo Ireland Oliver Loomes.
We are transforming our centuries-old vat houses, brew houses and cooperages into incredible spaces that will house and inspire a new generation of entrepreneurs, residents and visitors, dreamers and doers.


Decisions about the responsible design of artificial intelligence (AI) are often made by engineers with little training in the complex ethical considerations at play. Universities have struggled to find effective ways to integrate these issues into curricula for students in technical domains. In response, the Forum's Global Future Council on Artificial Intelligence and Robotics has recommended creating a repository of actionable and useful materials for faculty who wish to add social inquiry and discourse into their AI coursework.
Creating AI without considering the potential ethical and human-centred implications creates liabilities for the evolution of social, economic and governance systems. In view of the magnitude of risk and the central role that AI will have in ordering societal infrastructure, those responsible must be taught from the beginning how to design for healthy outcomes. This includes awareness raising, for example, ranging from data integrity and cultivating transparency to understanding how technical decisions relate to civil, social and geopolitical outcomes.
Teaching AI Ethics (TAIE) aims to connect a global group of university professors who teach in the area of AI and Machine Learning. The Forum is seeking to develop a community and repository of materials to help professors provide students with a critical awareness of how AI design decisions can influence social outcomes. The goal is to share materials, learn from one another and create best practice guides.
Professors teaching courses that touch on the social implications of AI are invited to share their materials, which will be placed in a Forum-hosted repository of curricula. This resource will guide those who have yet to develop learning materials on this topic. As professors new to the discipline develop their own curriculum, they will be encouraged to share these materials to foster collaboration.
As the community grows, members will be invited to participate in offline events geared towards community-building in AI education. The Forum hopes this platform will come to serve as a powerful mechanism for increasing knowledge and awareness about responsibly teaching AI.
If you are a University Professor working in this field please fill out the survey below to receive an invitation to join TAIE. You will receive access to our live repository of curricula and to a Forum-run community platform where you will be able to communicate with others in the community.
You may also see below for a public-facing set of sample curricula, which we will continue to curate from community submissions on an on-going basis.
This Project is co-created by World Economic Forum and Illah Nourbakhsh, Professor of Robotics and Jennifer Keating, Assistant Dean for Educational Initiatives at Carnegie Mellon University.


text:
Q: One line if in VB .NET Is it possible to do one line if statement in VB .NET? If so, how?

A: Or
IIf(CONDITION, TRUE_ACTION, FALSE_ACTION)

A: Just add Then:
If A = 1 Then A = 2

or:
If A = 1 Then _
    A = 2

A: One Line 'If Statement'
Easier than you think, noticed no-one has put what I've got yet, so I'll throw in my 2-cents.
In my testing you don't need the continuation? semi-colon, you can do without, also you can do it without the End If.
<C#> = Condition.
<R#> = True Return.
<E> = Else Return.
Single Condition
If <C1> Then <R1> Else <E>

Multiple Conditions
If <C1> Then <R1> Else If <C2> Then <R2> Else <E>

Infinite? Conditions
If <C1> Then <R1> Else If <C2> Then <R2> If <C3> Then <R3> If <C4> Then <R4> Else...
' Just keep adding "If <C> Then <R> Else" to get more

-Not really sure how to format this to make it more readable, so if someone could offer a edit, please do-

A: If (X1= 1) Then : Val1= "Yes" : Else : Val1= "Not" : End If

A: It's actually pretty simple..
If CONDITION Then ..INSERT CODE HERE..

A: Single line
Syntax:
If (condition) Then (do this)

Example:
If flag = true Then i = 1

Multiple ElseIf's
Syntax:
If (condition) Then : (do this)
ElseIf (condition2) Then : (do this)
Else : (do this)
End If

OR
If (condition) Then : (do this) : ElseIf (condition2) Then : (do this) : Else : (do this) : End If

Multiple operations
Syntax:
If (condition) Then : (do this) : (and this) : End If

A: At the risk of causing some cringing by purests and c# programmers, you can use multiple statements and else in a one-line if statement in VB. In this example, y ends up 3 and not 7.
i = 1
If i = 1 Then x = 3 : y = 3 Else x = 7 : y = 7

A: Use IF().
It is a short-circuiting ternary operator.
Dim Result = IF(expression,<true return>,<false return>)

SEE ALSO:

*

*IIF becomes If, and a true ternary operator

*Is there a conditional ternary
operator in VB.NET?

*Orcas introduces the IF operator - a
new and improved IIF

*The Ternary Operator in VB.NET

A: You can use the IIf function too:
CheckIt = IIf(TestMe > 1000, "Large", "Small")

A: Its simple to use in VB.NET code
Basic Syntax
IIF(Expression as Boolean,True Part as Object,False Part as Object)As Object

*

*Using IIF same as Ternary

*Dim myVariable as string= " "

*myVariable = IIf(Condition, True,False)

A: If (condition, condition_is_true, condition_is_false)

It will look like this in longer version:
If (condition_is_true) Then

Else (condition_is_false)

End If

redpajama_set_name: RedPajamaStackExchange


Catecholaminergic polymorphic ventricular tachycardia (CPVT) is a rare condition that has been associated with two genes that make proteins found inside the cell – the human ryanodine receptor (a calcium ion channel) and calsequestrin (a protein that interacts with the calcium channel). These regulate the release of calcium ions into the rest of the cell. If these do not function normally, the level of calcium inside the cell becomes too high, resulting in arrhythmias.
Some people with CPVT have no symptoms at all. Others may have palpitations (with or without an irregular heart beat), or blackouts while exerting themselves or suffering emotional stress. The condition may be found in most age groups but appears to be most severe in children and adolescents and in males.
Are there any physical signs?
There are no physical signs.
The diagnosis is usually made after the recording of arrhythmias that are characteristic of CPVT, while the person is doing exercise. The exercise ECG is therefore useful although some doctors use adrenaline testing as well. Genetic testing is of use as 1 in 2 people with the condition carry a ryanodine receptor mutation and are more likely to have blackouts or a cardiac arrest. When a member of a family has been found to carry a mutation, testing is then useful in detecting carriers who have not yet shown any signs of the condition.
Your doctor will advise you to take beta-blockers, to restrict the amount of exercise you do, and avoid medications that stimulate the heart. This combination can greatly improve the outlook for people with CPVT. Up to 1 in every 3 people with the condition, however, may also need to have an implantable cardioverter defibrillator (ICD) fitted, particularly if they have blackouts while taking beta-blockers.
Watch CRY's myheart cardiologist, Dr Michael Papadakis, talk about things to avoid if you have an ion-channel disease below.
Recently some doctors have used the cervical sympathectomy (already used in long QT syndrome) to treat CPVT with some success.


Are you looking for an English tutor who can help you improve your language skills? I am a Native English Speaker who can provide instruction to both secondary school students and adults. Perhaps you need some extra help with grammar and writing for a course or upcoming exam, wanting to improve your language and conversation skills for your work or business, or perhaps you just want to practice your skills for an upcoming holiday or vacation.
Tutoring students in Rijssen-Holten, Wierden, Nijverdal, Almelo, Hengelo, or Enschede.
I prefer to tutor in house but depending on the circumstances other arrangements can be made. Please contact me for information regarding rates.
If you are looking for assistance with editing or proofreading a thesis or manuscript please see the editing page.
I am also a Native Swedish Speaker and am available to tutor Swedish as well. Please contact me for more information.
...or through the contact form.


text:
Adrian Todaro
A World Bank report says that forest fires in Indonesia caused an economic loss of $5.2bn, which equals 0.5% of Indonesia's GDP.
Farmers in Indonesia burn the agricultural land in the dry season to prepare it for cultivation. The smoke from these fires affects other people and even other countries.
The World Bank assessed the impact of the fires in the eight affected districts between June and October 2019. Officials said that the losses might be even greater as the fires had raged through November.
The report says,
The forest and land fires, as well as the resulting haze, led to significant negative economic impacts, estimated at $157mn indirect damage to assets and $ 5.0bn from affected economic activities.
Over 900,000 people suffered respiratory diseases and 12 national airports and hundreds of schools had to be closed in Indonesia, Malaysia, and Singapore due to the smoke from the fires. Indonesian officials are blaming El-Nino weather patterns for amplifying the health effects of the forest fires this year.
Over 942,000 hectares of forest and agricultural land were burned in Indonesia this year. Additionally, 44% of the land burned were peatlands; thus, carbon emissions from the fires were double that from fires in the Amazon jungle earlier this year.
Thus, El-Nino and the burning of a large peatland area have caused a perfect storm that has engulfed not only Indonesia but its neighboring countries as well.
The report explicitly states that the fires are human-made and this problem has existed since 1997, hinting that successive Indonesian governments have dragged their feet on the matter, which has led to the current crisis.
About 720 megatonnes of carbon dioxide were released into the atmosphere due to the forest fires in Indonesia between January and November this year, according to the European Centre for Medium-Range Weather Forecast.
As a result of the fires, the World Bank has cut Indonesia's growth estimates by 0.09% in 2019 and 0.05% in 2020.
The World Bank report warns that the health effects from the fires could harm the global image of palm oil, the main commodity exported by Indonesia.


We provide delivery to any place in the UK. We try to quarantee the shortest possible delivery time to our customers. We also quarantee safe delivery to England, Scotland and Wales with our own fleet of cars regardless of the order size. All of the offered products come with 2 year warranty.
We will contact you the day before planning delivery. You will be informed about estimated hour of delivery.
Due to the fact that our driver delivers products to several customers, please be prepared for furniture collection - provide two people to carry funiture to your home / flat.
NOTICE! Our drives are no oblidged to carry furniture to your home / flat. Carrying products is subject to driver's decision. Carrying service is not included in delivery costs.
Approx. delivery time for flat pack furniture (chest of drawers, wall units, wardrobes, bedroom furniture) is about 15-40 working days - many products are in stock so please contact us before purchase.
Approx. delivery time for upholstery (lounge sets, sofas, couches, corner sofas, chairs and tables) is about 20-40 workig days.
During pre- holiday seasons (before Christmas, Easter) delivery time can be prolonged for 5-10 working days.


The skin is the largest organ in the body and acts as a barrier to chemical and environmental factors in order to protect it. The science behind an amazing tan comes from a cell in the skin called a 'melanocyte'. These are situated in the epidermis (top layer) of the skin and are made up of an amino acid called L-Tyrosine which is responsible for causing pigmentation and colour to the skin. When your skin is exposed to the sun, a Melanocyte-stimulating hormone comes into action and stimulates L-Tyrosine to produce more melanin via a series of reaction in the skin and communication between different cells, which eventually leads to a suntan.
– If you are regularly exposed to the sun or sunbeams then it is important to get regular skin checks; be cautious of any mole irregularities, changes, itching or bleeding.
If you are really sporty and spend a lot of time doing activities in the summer (such as swimming, surfing, cycling etc.), a water-resistant sunscreen is essential, as water and sweat affect sunscreen, meaning it won't last as long. It is important to remember water-resistant does not mean waterproof; water-resistant sunscreens will protect you for around 40-80 minutes longer than standard sun protection but should be reapplied once you have left the water and dried off.
For those who love to tan, use a high factor, broad-spectrum sunscreen not only to stop you from burning but also to prevent premature aging and exposure to UVA rays. I see many people in their 40's and 50's who admit to loving the sun but are not using adequate sunscreen and come to me looking for anti-aging treatments. Skin damage won't show straight away but will show later in life, therefore prevention is better than cure.
If you have paler skin tones and spend lots of time in the shade, this doesn't mean you can skip using sunscreen; paler skin types burn easily and are more at risk from sun damage, therefore, need an SPF 30 or higher. Cloudy days are also not a safe bet at 80% of the sun's rays can still penetrate the skin.
If you have darker skin tones, then you may tan easily and rarely burn as your skin has more natural pigmentation, and therefore have more natural protection from the sun. Your skin is still prone to sun damage and also at risk of more serious types of skin cancer like melanoma, therefore a sunscreen of SPF 15 or higher is still important.
A great option for men with an oily, sometimes greasy complexion, this very reasonably priced face cream from Garnier is actually perfect for year-round use, yes guys it's not just about the summer months. If you want to avoid going wrinkly early doors, then get in the habit of protecting on a 365 basis. This non-comedogenic formula is enriched with salicylic acid and ginger root extracts, great for blemish prone skin and with a mattifying effect for up to 8hrs it protects against the harmful UVB and UVA damage.
Ok if you're late to the suncare party and are already seeing signs of damage then this little number from Ultrasun could be just the ticket. Designed to specifically target skin pigmentation it also works as a moisturiser reducing fine lines and wrinkles, all the while offering factor 50 protection from the suns harmful rays. A great addition to your travel wash bag.
What Kiehl's don't know about skincare, frankly isn't worth knowing and if you're looking for some lightweight protection for these balmy British days then this non-greasy broad spectrum formula is good an option as you'll find. For many blokes, the key is avoiding a heavy thick sunscreen that clogs the pores and leads to a sweating and shiny face. With the addition of wrinkle reducing, dark spot protecting action, this sun cream is worth the wonga.
This award-winning, organic, antioxidant-rich formula is perfect for those with a propensity for an active lifestyle and anyone spending long periods in the gaze of the glaring sun. Water resistant for up to 80 minutes this fast absorbing, lightweight cream also contains Evening Primrose Oil and Linseed Oil for antioxidant protection while the addition of Safflower offers a moisturising effect all while not feeling heavy in texture. A powerhouse in the suncare department.
Another great value for money option is this lotion from La Roche-Posay that is ideal for normal/combination skin, with it's easily absorbed texture and lightweight formula it is also water resistant. Perfect for those younger men looking for an invisible finish that has high dose protection, great as a preventative measure for those looking to maintain their youthful, boyish charms well into later life.


text:
The latest updates and breaking news on Intellectual Property from around the world
List by category
Case Law Civil Procedure Companies Consumer Law Contract Copyright Defamation Designs Digital/Tech EU/International Legal News News Passing Off Patents Regulatory Trade Marks
Dyson Look To Clean Up
The leading manufacturer of household appliances, Dyson, is bringing a legal claim against their former chief executive Max Conze for an alleged series of breaches, after he steppe...
BBC Facing Cosby Copyright Case
Carsey-Werner, the producer of the popular 1980s American television sitcom 'The Cosby Show', has brought a copyright case against the BBC. They have alleged copyright infringement...
ResearchGate Takes Step In The Right Direction
You may remember a few weeks ago we wrote an article on ResearchGate, the social networking site for academics to share published papers and books with one another, and the copyrig...
IP Crime Report highlights challenge of internet infringers
The UK Intellectual Property Office has published its IP Crime and Enforcement report for 2016-2017 (the Report). The Report explains the current challenges and threats posed by in...
Eminem's success against NZ political party
Eminem, the American award-winning rapper, songwriter and producer, has been the latest artist to have copyright in his music infringed. The Judgment from a May 2017 trial in a cop...
Disney Hope For A Happy Ever After
Disney is well known for taking its intellectual property rights seriously and defending their brand by suing anyone that dares to step on their toes. Most cases go unheard of as D...
Aboriginal artist's family battle for copyright
Albert Namatjira, the Australian aboriginal artist who died in 1959, made headlines this week after it was announced that the copyright in his artwork has finally been returned to ...
Blurred lines Case Appears No Clearer
The infamous 'Blurred Lines' verdict which ultimately decided that musicians Pharrell Williams and Robin Thicke were guilty of copying Marvin Gaye's 1977 hit, 'Got to give it up' h...
ResearchGate Faces Large Copyright Case
ResearchGate is a social networking site based in Berlin. It allows academics to share published papers, presentations and book chapters with millions of its members. The firm was ...
Pepe the Frog's creator goes after the 'alt-right'
The so-called Alt-right is a political movement which seems to be having a major impact on world events, most famously in the election of Donald Trump as President of the USA in 20...
Parties Overcome Song Copyright
'We Shall Overcome' the famous civil rights movement song, which has been called the most powerful song of the 20th Century has been the subject of a copyright dispute in the USA. ...
Monkey 'Selfie' Ownership Finally Settled
We have previously written about the rather improbable case of a photographer being sued by a monkey for copyright infringement. The case has now finally been settled after a 2 yea...


We can custom build you a Milano Leather Ottoman for your living room in various imported leathers. Rectangular or Square ottomans are available in various sizes. Hair-on-Hide leather is optional.
The matching ottoman for the Milano Style Sofa.
The Milano is one of our many custom leather furniture styles.
See the full line of Milano furniture.


Recently I have taken the "VIA Signatura Strengths Questionnaire" which is a scientific research-based test that measures 24 character strengths. It takes nearly 40 minutes and includes 240 questions. Here are my results, what about yours?


Toyota and ALBERT have agreed on a business alliance for big data analysis—primarily in the field of advanced development of automated driving technology—and Toyota will invest in ALBERT.
Toyota Motor Corporation and ALBERT Inc. announced an agreement on a business alliance for big data analysis—primarily in the field of advanced development of automated driving technology—and that Toyota will invest in ALBERT. Toyota's investment in ALBERT is expected to be in the amount of 400 million yen, and Toyota is to acquire new shares in ALBERT issued through a third-party allocation of shares dated May 30, 2018.
ALBERT has been actively expanding into the field of imagery analysis in the development of automated driving technologies. Through the business alliance, Toyota believes it will be possible to strengthen elements such as data analysis processes in Toyota's development of AI technologies, which is expected to accelerate its development of automated driving technologies.
Executive General Manager Ken Koibuchi, who is in charge of the development of automated driving at Toyota's in-house Advanced R&D and Engineering Company, commented, "We believe that AI technologies are indispensable for achieving our vision of 'safe and smooth mobility for all people.' To bring out the full performance of AI technologies, it is necessary to skillfully manage large volumes of data. I look forward to this business alliance accelerating Toyota's development of automated driving technologies."
ALBERT President Takeshi Matsumoto said, "For technological innovation, such as in the development of automated driving technologies, to be fully implemented in society and be able to create new value, advanced analytical capacity centered on AI and machine learning and data scientists who pursue realization of this are essential. Going forward, our company intends to support 'safe technological innovation demanded by society' through, among other efforts, the strengthening of a distinguished group of data scientists who aim for enhanced analysis."


text:
Intellectual Property, and Fragrances: Does Protection Exist?
Home → Legal → Intellectual Property, and Fragrances: Does Protection Exist?
The fragrance industry is constantly changing and has made significant advances since it began in the South of France during the 19th century. Technological advances have created a fragrance industry that today is more vulnerable than ever to appropriation of formulas and other information that is intended to remain secretive. Knowledge, particularly of specific formulas or manufacturing processes for fragrances are considered the most valuable assets in the industry because companies tend to focus their investments in these areas. Unfortunately, reverse engineering technology has made these formulas relatively easy for competitors to obtain. Thus, in recent years, the fragrance industry is gaining momentum in its pursuit for new forms of legal protection for its information assets. Although IP protection is limited for fragrances, at Amazon Sellers Lawyer we see complaints by brand owners against Amazon Sellers all the time.
Patent Protection:
Today, there are a handful of fragrance and flavor companies which develop and manufacture almost all of the fragrances sold under the names of luxury brands, fashion designers, celebrities, etc. These fragrances ultimately end up in everyday products like candles, colognes and perfumes and are packaged in distinctive bottles. While it seems that most of these fragrances end up in glamorous or designer focused products, the reality is that fragrances are more typically found in detergents, cleaning supplies or air fresheners.
Although, many of the fragrance based products undoubtedly are useful, the fragrance industry typically does not rely on patent law for protection. This is because the fragrances produced are highly valuable. Thus, their market value goes well beyond the 20-year protection provided by a patent before patent law would require the fragrance formula to be revealed. Popular fragrances like Chanel's No. 5 have enjoyed popularity and success for decades.
There are a few manufacturers who have successfully obtained utility patents for fragrances, but these manufacturers were able to make claims of therapeutic efficacy for their scents. Patent law is intended to protect new, innovative, and useful products, but patents do not provide protection for the thousands of original fragrances which are ultimately used in a variety of consumer products. Thus, patent law provides insufficient protection to the fragrance industry.
Copyright Protection:
Music is something that almost everyone seems to think of when considering Copyright protection. Like a musician writing a new song, a skilled perfume creator will draw from an array of scented essences and create a combination in an effort to create an original fragrance. "The intensity of a particular component of a fragrance is referred to as its "volume", and the perfumer's improvisations are tested using paper strips known as "touches" or piano keys. Not surprisingly, some of the results of these combinations of scents have been named with musical terms like Arpège and Sonata."
Musical compositions, once recorded as sound or written as sheet music, contain original forms of expression created by the musician and are thus eligible for copyright protection. It would seem logical then, that new fragrances, should also be eligible for copyright protection. However, this is not the case. The aim of any fragrance creator is to evoke emotional responses through their interaction with the consumer's sense of smell. This is true whether the fragrance is ultimately to be used in a designer perfume, or in a laundry detergent.
Copyright law has expanded dramatically in the 21st century, to the point where cartoon characters and action figures are copyrightable subject matter, but it still does not seem to have caught up to fragrances. Thus, copyright law also fails to adequately protect the fragrance industry.
Trademark / Scent mark:
Trademarks are typically symbols or marks that are afforded protection because they are commonly associated with certain brands as indicators of their source or quality. Like trademarks, scents can act as identifiers for certain products as well. Certain consumers can unmistakably distinguish between their favorite designer perfumes. However, scents are difficult to trademark because trademark protection requires some sort of a nonfunctional and distinctive aspect. This requirement is difficult to satisfy because fragrance based products are typically always functional. Candles, air fresheners, perfumes and colognes all function to emit pleasant scents and evoke sensational reactions in those who smell them. As such, trademark law also fails to adequately protect fragrances.
Proving Non-Functionality
In the United States there is a high bar to overcome for scent mark protection. The applicant must be able to show: (1) non-functionality; and (2) distinctiveness. A product feature is functional if it is "essential to the use or purpose of the article or if it affects the cost or quality of the article." Qualitex Co. v. Jacobson Products Co., 514 U.S. 159, 165 (1995) (quoting Inwood Laboratories, Inc. v. Ives Laboratories, Inc., 456 U.S. 844, 850 n.10 (1982)). The purpose of the functionality requirement is to prevent a trademark owner from controlling a useful product feature. If an applicant can somehow show that their scent acts as a product's source identifier and performs no function, they may be able to obtain trademark protection. However, because almost every fragrance product performs the core function of emitting a scent, this requirement is almost never met.
What does this mean for Amazon Sellers?
At Amazon Sellers Lawyer, we have several clients who make a living selling fragrance based products on the platform. While these fragrances or scents themselves are almost never afforded intellectual property protections, this does not mean that sellers will be immune from complaints from brand owners. We have been successful helping our clients remove baseless trademark complaints, but some brands are more difficult to deal with than others. Intellectual property law is evolving today more than ever, and fragrance protection has become a highly debated topic. As the law is bound to change and is becoming increasingly more complex than it already stands, it is more important than ever to be educated. Should you receive an Amazon Seller Suspension due to a fragrance based product complaint, it is essential to know and use the law when drafting your plan of action. Amazon Sellers Lawyer is here to help.
On March 20, 2017 / Legal