On decidability of recursive weighted logics

Abstract

In this paper, we develop and study two recursive weighted logics (RWLs) $\mathcal {L}^w$ and $\mathcal {L}^t$, which are multi-modal logics that express qualitative and quantitative properties of labelled weighted transition systems (LWSs). LWSs are transition systems describing systems with quantitative aspects. They have labels with both actions and real-valued quantities representing the costs of transitions with respect to various resources. RWLs use first-order variables to measure local costs. The main syntactic operators are similar to the ones of timed logics for real-time systems. $\mathcal {L}^w$ has operators that constrain the value of resource-variables at the current state. $\mathcal {L}^t$ extends $\mathcal {L}^w$ by having quantitative constraints on the transition modalities as well. This extension makes sure that $\mathcal {L}^t$ is adequate, i.e. the semantic equivalence induced by $\mathcal {L}^t$ coincides with the weighted bisimilarity of LWSs. In addition, our logic is endowed, with simultaneous recursive equations, which allow encoding of properties of infinite behaviours. We prove that unlike in the case of the timed logics, the satisfiability problems for RWLs are decidable. The proofs use a variant of the region construction technique used in the literature with timed automata, which we adapt to the specific settings of RWLs. For $\mathcal {L}^t$, we also propose an attractive alternative proof which makes use of the algorithm for $\mathcal {L}^w$.

1 Introduction

Formal specification, verification and analysis of behavioural properties of software-based systems have emerged as a useful method for validating a design before the implementation of the system has started. However, in the setting of embedded software systems or cyber–physical systems, the correctness is intimately linked to the resource constraints of the execution platform as well as quantitative aspects of the physical environment to be controlled. Hence, specification and verification should not only consider functional properties (correctness, predictability, etc) but also non-functional properties such as those related to resource constraints (time, energy, bandwidth, etc). To deal with the growing complexity of embedded systems—in size as well as in features—there is a pressing need for tools that provide computer assistance to the verification and analysis, with the area of model checking providing a number of such fully automated tools. Within model checking, various state machine-based modelling formalisms have surfaced, which allow for such quantitative aspects to be expressed, especially time constraints, with the well-established notion of timed automata (Alur and Dill 1990) being ideal for modelling such aspects. Time is, however, not the only quantity that is relevant for embedded systems; another important quantitative aspect is energy, which may be consumed or—for certain systems—harvested. Here, the extension to weighted timed automata (Behrmann et al. 2001; Alur et al. 2001) allows for such constraints to be modelled and efficiently analysed.

In this paper, we put forward the notion of labelled weighted transition systems (LSW) as the semantics foundation for models of systems with quantitative aspects. More precisely, an LWS is a labelled transition system that has a number of resources, which allow us to model the quantitative consumptions of resources. Its transitions are labelled at the same time with both actions and real values, representing the costs of the corresponding transitions in terms of resources. Note that our notion of weighted transition systems can also be infinite and/or infinitely branching and thus is more general than weighted automata (Droste et al. 2009). In order to use a variant of the region construction technique developed for timed automata in (Alur and Dill 1990; Alur et al. 1990), we only consider non-negative labels in this paper.

In order to specify and reason about not only the qualitative but also about quantitative properties of the systems, we consider two recursive weighted logics (RWL)—$\mathcal {L}^w$ and $\mathcal {L}^t$—semantically to be interpreted over LWSs. The RWLs are extensions of the weighted modal logic (Larsen and Mardare 2014) with maximal fixed points. The maximal fixed points—which are defined by simultaneous recursive equations (Larsen 1990; Cleaveland et al. 1992; Cleaveland and Steffen 1993) in this paper—allow encoding of properties of infinite behaviours including safety and cost-bounded liveness. They specify the weakest properties satisfied by the recursive variables.

Resource constrains in RWLs are encoded by the use of resource-variables, similar to the clock-variables used in the timed logics (Alur et al. 1993a; Henzinger et al. 1992; Aceto et al. 2007). We use resource valuation to assign non-negative real values to resource-variables. In previous work (Larsen et al. 2014b), we restricted our attention to only one resource-variable for each type of resources. This guaranteed the decidability of the logic and the finite model property. However, this restriction bounds severely the expressiveness of the logic. Consider as an example a quantitative system performing the actions a, b, c and d in sequence, but with the additional constraint that the energy consumption between a and c should be at most 2 joule, and the energy consumption between b and d should be at least 3 joule. Given the overlap between the two energy-constrained phases $a--c$ and $b--d$, this property cannot be specified by the logic with only one resource-variable for each type of resources, because we need two resource-variables to measure the same resource—energy in this example.

In this paper, we allow multiple resource-variables for each type of resource, which measure the resource in different ways. For both $\mathcal {L}^w$ and $\mathcal {L}^t$, we discuss the event-related resource-variables. More precisely, for each type of resource and each action, we associate one resource-variable. Whenever the system performs one action, all the resource-variables associated with this action are reset to zero after the corresponding transition, meaning that the resource valuation will map those resource-variables to zero.

RWLs are endowed with modal operators that constrain the values of resource-variables, allowing us to specify and reason about the quantitative properties related to resources, e.g. energy and time. While in an LWS we can have real-valued labels, the modalities of the logics only encode rational values. This will not limit too much the expressive power of RWLs, because a real-valued resource can be characterized by using an infinite convergent sequences of rationals approximating it.

$\mathcal {L}^w$ has operators that constrain the value of resource-variables at the current state. However, the logic does have no means of constraining the resource consumption of transitions. Whereas $\mathcal {L}^w$ can be used to encode various interesting scenarios, it is not adequate in the sense that it is not sufficiently expressive to characterize weighted bisimulation. The logic $\mathcal {L}^t$ extends $\mathcal {L}^w$ by having quantitative constraints on the transition modalities as well. As an important result of the paper, we prove that $\mathcal {L}^t$ is adequate, i.e. the semantic equivalence induced by $\mathcal {L}^t$ coincides with the weighted bisimilarity of LWSs.

Even though $\mathcal {L}^w$ is the least expressive of the two logics discussed in this paper, we shall see that it fails to enjoy the finite model property! However, as another important result of the paper, we demonstrate how to apply a variant of the region construction technique developed for timed automata (Alur and Dill 1990; Alur et al. 1990; Laroussinie et al. 1995), to obtain symbolic LWSs of the satisfiable formulas. These symbolic LWSs provide an abstract semantics for LWSs, allowing us to reason about satisfiability by investigating the symbolic models that are finite. We have proposed a model construction algorithm, which constructs a symbolic LWS for a given satisfiable (consistent) $\mathcal {L}^w$ formula. The symbolic model can be eventually used to determine the existence of the concrete LWSs and generate them—possibly infinite—which are models of the given formula.

The satisfiability problem of $\mathcal {L}^t$ can be solved in a similar way with $\mathcal {L}^w$. However, an attractive alternative is to firstly encode the problem for $\mathcal {L}^t$ into one similar to that of $\mathcal {L}^w$ by translating the given $\mathcal {L}^t$ formula into $\mathcal {L}^w$ with a special 0-cost action and then use the model construction algorithm with a minor modification to check the satisfiability of this $\mathcal {L}^w$ formula, and if the $\mathcal {L}^w$ formula is not satisfiable, then the given $\mathcal {L}^t$ formula is not satisfiable either; otherwise, the given $\mathcal {L}^t$ formula is satisfiable and we finally generate the model for it according to the model for the corresponding $\mathcal {L}^w$ formula.

The satisfiability problem is known to be undecidable for logics very similar to ours, such as TCTL (Alur et al. 1993b), T$_\mu$ (Henzinger et al. 1992), L$_\nu$ (Laroussinie et al. 1995) and timed modal logic (TML) (Larsen et al. 2014a). Therefore, our decidability results are quite important and, in a sense, surprising.

The paper is organized as follows: in the following section, we present the notion of labelled weighted transition system together with weighted bisimulation; in Sect. 3, we introduce the recursive weighted logic $\mathcal {L}^w$ with its syntax and semantics; Sect. 4 is dedicated to the region construction technique and the symbolic models of LWSs; in Sect. 5, we prove the decidability of the satisfiability problem for $\mathcal {L}^w$; in Sect. 6, the more expressive recursive weighted logic $\mathcal {L}^t$ is introduced, together with the adequacy problem and the satisfiability problem being solved. The paper also includes a conclusive section where we summarize the results and describe future research directions.

This paper is an extension of our previous work that has been presented at ICTAC2014 (Larsen et al. 2014c).

2 Labelled weighted transition systems

A labelled weighted transition system (LWS) is a transition system that has several types of resources (e.g. energy, price, time, bandwidth, etc.) and has the transitions labelled both with actions and (non-negative) real numbers. In Fig. 1 is represented such a system in which there are three types of resource; each number is used to represent the cost of the corresponding transitions in terms of one type of resource.

Definition 1

(Labelled Weighted Transition System) A labelled weighted transition system is a tuple

$$\begin{aligned} \mathcal {W}=(M,{\mathcal {K}},\Sigma ,\theta ) \end{aligned}$$

where M is a non-empty set of states, ${\mathcal {K}}=\{e_1,\ldots ,e_k\}$ is a finite set of (k types of) resources, $\Sigma$ a non-empty set of actions and $\theta : M \times (\Sigma \times [{\mathcal {K}}\rightarrow \mathbb {R}_{\ge 0}])\rightarrow 2^M$ is the labelled transition function, where $[{\mathcal {K}}\rightarrow \mathbb {R}_{\ge 0}]$ represents the set of functions from ${\mathcal {K}}$ to non-negative reals.

Fig. 1

Labelled weighted transition system

For simplicity, hereafter we represent the function $f:{\mathcal {K}}\rightarrow \mathbb {R}_{\ge 0}$ defined by $f(e_i)=r_i$ for all $i=1,\ldots ,k$, using the real values vector ${\overline{u}}=(r_1,\ldots ,r_k)\in \mathbb {R}_{\ge 0}^k$. For ${\overline{u}}\in \mathbb {R}_{\ge 0}^k$, we use ${\overline{u}}(e_i)$ to denote the i-th component of the vector ${\overline{u}}$, i.e. the cost of the resource $e_i$ during the transition.

Instead of $m'\in \theta (m,a,{\overline{u}})$, we write $m\xrightarrow {{\overline{u}}}_{a}m'$.

To clarify the role of the aforementioned concepts, consider the following example.

Example 1

In Fig. 1, we show the LWS

$$\begin{aligned} \mathcal {W}=( M ,{\mathcal {K}},\Sigma ,\theta ), \end{aligned}$$

where $M =\{m_0,m_1,m_2\}, {\mathcal {K}}=\{e_1,e_2,e_3\}, \Sigma =\{a,b\}$, and $\theta$ defined as follows: $m_0\,{\xrightarrow {(3,4,5)}_{a}}\, m_1, m_0\,{\xrightarrow {(\pi ,\pi ,0)}_{b}}\, m_2$ and $m_1\,{\xrightarrow {(\sqrt{2},1.9,7)}_{a}}\, m_2$.

$\mathcal {W}$ has three states—$m_0,m_1,m_2$, three kinds of resource—$e_1,e_2,e_3$ and two actions—a, b. The state $m_0$ has two transitions: one a-transition to $m_1$—which costs 3 units of $e_1$, 4 units of $e_2$ and 5 units of $e_3$, and one b-transition to $m_2$—which costs $\pi$ units of $e_1$ and $e_2$, respectively (and 0 units of $e_3$). If the system does an a-transition from $m_0$ to $m_1$, the amounts of the resource $e_1$, $e_2$ and $e_3$ increase with 3, 4 and 5 units, respectively.

The concept of weighted bisimulation is a relation between the states of a given LWS that equates states with identical (action and weighted) behaviours.

Definition 2

(Weighted Bisimulation)

Given an LWS $\mathcal {W}=( M ,{\mathcal {K}},\Sigma ,\theta )$, a weighted bisimulation is an equivalence relation $R\subseteq M \times M$ such that whenever $(m,m')\in R$,

• if $m\xrightarrow {{\overline{u}}}_{a}m_1$, then there exists $m_1'\in M$ s.t. $m'\xrightarrow {{\overline{u}}}_{a}m_1'$ and $(m_1,m_1')\in R$;

• if $m'\xrightarrow {{\overline{u}}}_{a}m_1'$, then there exists $m_1\in M$ s.t. $m\xrightarrow {{\overline{u}}}_{a}m_1$ and $(m_1,m_1')\in R$.

If there exists a weighted bisimulation relation R such that $(m,m')\in R$, we say that m and $m'$ are bisimilar, denoted by $m\sim m'$.

Fig. 2

Weighted bisimulation

As for the other types of bisimulation, the previous definition can be extended to define the weighted bisimulation between distinct LWSs by considering bisimulation relations on their disjoint union. Weighted bisimilarity is the largest weighted bisimulation relation; if $\mathcal {W}_i=( M _i,{\mathcal {K}}_i,\Sigma _i,\theta _i)$, $m_i\in M _i$ for $i=1,2$ and $m_1$ and $m_2$ are bisimilar, we write

$$\begin{aligned} (m_1,\mathcal {W}_1)\sim (m_2,\mathcal {W}_2). \end{aligned}$$

The following examples show the role of the weighted bisimilarity.

Example 2

In Fig. 2, $\mathcal {W}_1=( M _1,{\mathcal {K}}_1,\Sigma _1,\theta _1)$ is an LWS with five states and one type of resources, where

$$\begin{aligned} M _1=\{m_0,m_1,m_2,m_3,m_4\}, \end{aligned}$$

$\Sigma _1=\{a,b,c,d\}$, ${\mathcal {K}}_1=\{e\}$ and $\theta _1$ is defined as: $m_0\xrightarrow {3}_{a}m_1$, $m_0\xrightarrow {2}_{b}m_2$, $m_1\xrightarrow {0}_{d}m_2$, $m_1\xrightarrow {3}_{c}m_3$, $m_2\xrightarrow {0}_{d}m_1$ and $m_2\xrightarrow {3}_{c}m_4$. It is easy to see that $m_3\sim m_4$ because neither of them can do any transition. Besides, $m_1\sim m_2$ because both of them can do a c-transition with cost 3 to some states which are bisimilar ($m_3$ and $m_4$) and a d-action transition with cost 0 to each other. $m_0$ is not bisimilar to any states in $\mathcal {W}_1$.

$\mathcal {W}_2=( M_2,{\mathcal {K}}_2,\Sigma _2,\theta _2)$ is an LWS with three states, where $M _2=\{m_0',m_1',m_2'\}$, $\Sigma _2=\Sigma _1$ ${\mathcal {K}}_2={\mathcal {K}}_1$ and $\theta _2$ is defined as: $m_0'\xrightarrow {3}_{a}m_1'$, $m_0'\xrightarrow {2}_{b}m_1'$, $m_1'\xrightarrow {0}_{d}m_1'$ and $m_1'\xrightarrow {3}_{c}m_2'$.

We can see that:

$$\begin{aligned} \begin{array}{lll} (m_0,\mathcal {W}_1)&{}\sim &{}(m_0',\mathcal {W}_2),\\ (m_1,\mathcal {W}_1)&{}\sim &{}(m_1',\mathcal {W}_2),\\ (m_2,\mathcal {W}_1)&{}\sim &{}(m_1',\mathcal {W}_2),\\ (m_3,\mathcal {W}_1)&{}\sim &{}(m_2',\mathcal {W}_2),\\ (m_4,\mathcal {W}_1)&{}\sim &{}(m_2',\mathcal {W}_2). \end{array} \end{aligned}$$

Notice that

$$\begin{aligned} (m_0'',\mathcal {W}_3)\not \sim (m_0',\mathcal {W}_2), \end{aligned}$$

because

$$\begin{aligned} (m_1'',\mathcal {W}_3)\not \sim (m_1',\mathcal {W}_2). \end{aligned}$$

Besides, $m_1''\not \sim m_2''$, because $m_1''$ can do a d-action with weight 2 while $m_2''$ cannot and $m_2''$ can do a d-action with weight 1 while $m_1''$ cannot.

3 Recursive weighted logic $\mathcal {L}^w$

In this section, we introduce the first recursive weighted logic (RWL) we study in this paper, denoted by $\mathcal {L}^w$, which encodes properties of LWSs.

To encode various resource constrains in $\mathcal {L}^w$, we use resource-variables, similar to the clock-variables used in timed logics (Alur et al. 1993a; Henzinger et al. 1992; Aceto et al. 2007). In this section, we introduce event-related resource-variables to measure the resources in different ways corresponding to different actions, i.e. for each action $a\in \Sigma$, we associate resource-variables $x_a^{1},\ldots ,x_a^{k}$ for each type of resource $e_1,\ldots ,e_k$, respectively. In the following, we use

$$\begin{aligned} {\mathcal {V}}_i=\{x_a^{i}\mid a\in \Sigma \} \end{aligned}$$

to denote the set of the resource-variables associated for the type of resource $e_i$,

$$\begin{aligned} {\mathcal {V}}_a=\{x_a^{i}\,\mid \, i=1,\ldots ,k\} \end{aligned}$$

to denote the set of the resource-variables associated with the action a and

$$\begin{aligned} {\mathcal {V}}=\bigcup _{i=1,\ldots ,k}{\mathcal {V}}_i =\bigcup _{a\in \Sigma }{\mathcal {V}}_{a} \end{aligned}$$

to denote the set of all the resource-variables.

Note that:

• 1. for any i, j such that $i\not =j$, ${\mathcal {V}}_i\cap {\mathcal {V}}_j=\emptyset$,

  and for any a, b such that $a\not =b$, ${\mathcal {V}}_a\cap {\mathcal {V}}_b=\emptyset$;

• 2. $|{\mathcal {V}}_i|=|\Sigma |\, {\hbox {for any}} \,i\in \{1,\ldots ,k\},$

  $|{\mathcal {V}}_a|=k\,{\hbox {for any a}}\,\in \Sigma ,$

  $|{\mathcal {V}}|=|\Sigma |\times k.$

In addition to the classic boolean operators (except negation), our logic $\mathcal {L}^w$ is firstly endowed with a class of recursive (formula) variables $X_1,\ldots , X_n$, which specify properties of infinite behaviours. We denote by ${\mathcal {X}}$ the set of recursive formula variables.

Secondly, $\mathcal {L}^w$ is endowed with a class of modalities, named transition modalities, of type [a] or $\langle a\rangle$, for $a\in \Sigma$, which are defined as the classical transition modalities with reset operation of all the resource-variables associated with the corresponding action followed. More precisely, every time the system does an a-action; all the resource-variables $x\in {\mathcal {V}}_a$ will be reset after this transition, i.e. x is interpreted to zero after every a-action, for all $x\in {\mathcal {V}}_a$.

Besides, $\mathcal {L}^w$ is also endowed with a class of modalities of arity 0 called state modalities of type $x\bowtie r$, for $r\in \mathbb {Q}_{\ge 0}$, $x\in {\mathcal {V}}$ and $\bowtie \ \in \{\le ,\ge ,<,>\}$, which predicates about the value of the resource-variable x at the current state.

Before proceeding with the introduction of the maximal fixed points, we firstly define the basic formulas of $\mathcal {L}^w$ and their semantics. Based on them, we will eventually introduce the recursive definitions—the maximal equation blocks—which extend the semantics of the basic formulas.

Definition 3

(Syntax of $\mathcal {L}^w$ Basic Formulas) For arbitrary $r\in {\mathbb {Q}_{\ge 0}}$, $a\in \Sigma$, $x\in {\mathcal {V}}$, $\bowtie \ \in \{\le ,\ge ,<,>\}$ and $X\in {\mathcal {X}}$, let

$$\begin{aligned} \mathcal {L}:~~~\phi :=~\top ~|~\bot ~|~x\bowtie r~|~\phi \wedge \phi ~|~\phi \vee \phi ~|~[a]\phi ~|~\langle a\rangle \phi ~|~X. \end{aligned}$$

Before introducing the semantics for the basic formulas, we define the notion of resource valuation and extended states.

Definition 4

(Resource Valuation) A resource valuation is a function $l:\mathcal V\rightarrow \mathbb {R}_{\ge 0}$ that assigns (non-negative) real numbers to the resource-variables in $\mathcal V$.

A resource valuation assigns non-negative real values to all the resource-variables, and the assignment is interpreted as the amount of resources measured by the corresponding resource-variable in a given state of the system. We denote by L the class of resource valuations.

We write $l_i$ to denote the valuation for all resource-variables $x\in {\mathcal {V}}_i$ under the resource valuation l, i.e. for any $x\in {\mathcal {V}}$,

$$\begin{aligned} \begin{array}{lll} l_i(x)&{}=&{}\left\{ \begin{array}{lll} l(x),&{}&{}x\in {\mathcal {V}}_i\\ \text {undefined},&{}&{}\text {otherwise} \end{array}\right. \end{array} \end{aligned}$$

Similarly, we write $l_a$ to denote the valuation for all resource-variables $x\in {\mathcal {V}}_a$ under the resource valuation l, i.e. for any $x\in {\mathcal {V}}$,

$$\begin{aligned} \begin{array}{lll} l_a(x)&{}=&{}\left\{ \begin{array}{lll} l(x),&{}&{}x\in {\mathcal {V}}_a\\ \text {undefined},&{}&{}\text {otherwise} \end{array}\right. \end{array} \end{aligned}$$

If l is a resource valuation and $x\in \mathcal V, s\in \mathbb {R}_{\ge 0}$ we denote by $l[x\mapsto s]$ the resource valuation that associates the same values as l to all variables except x, to which it associates the value s, i.e. for any $y\in {\mathcal {V}}$,

$$\begin{aligned} \begin{array}{lll} l[x\mapsto s](y)&{}=&{}\left\{ \begin{array}{lll} s,&{}&{}y=x\\ l(y),&{}&{}\text {otherwise} \end{array}\right. \end{array} \end{aligned}$$

Moreover, for ${\mathcal {V}}'\subseteq {\mathcal {V}}$ and $s\in \mathbb {R}_{\ge 0}$, we denote by $l[{\mathcal {V}}'\mapsto s]$ the resource valuation that associates the same values as l to all variables except those in ${\mathcal {V}}'$, to which it associates the value s, i.e. for any $y\in {\mathcal {V}}$,

$$\begin{aligned} \begin{array}{lll} l[{\mathcal {V}}'\mapsto s](y)&{}=&{}\left\{ \begin{array}{lcl} s,&{}&{}y\in {\mathcal {V}}'\\ l(y),&{}&{}\text {otherwise} \end{array}\right. \end{array} \end{aligned}$$

For ${\overline{u}}\in \mathbb {R}_{\ge 0}^k, l+{\overline{u}}$ is defined as: for any $i\in \{1,\ldots ,k\}$, for any $x\in {\mathcal {V}}_i$,

$$\begin{aligned} (l+{\overline{u}})(x)=l(x)+{\overline{u}}(e_i). \end{aligned}$$

A pair (m, l) is called extended state of a given LWS $\mathcal {W}=( M, {\mathcal {K}},\Sigma , \theta )$, where $m\in M$ and $l\in L$. Transitions between extended states are defined by:

$$\begin{aligned} (m,l)\rightarrow _{a}(m',l')\text { iff }m\xrightarrow {{\overline{u}}}_{a}m'\text {and }l'=(l +{\overline{u}})[{\mathcal {V}}_a\mapsto 0]. \end{aligned}$$

Given an LWS $\mathcal {W}=( M ,{\mathcal {K}},\Sigma ,\theta )$, we interpret the $\mathcal {L}^w$ basic formulas over an extended state (m, l) and an environment $\rho$ which maps each recursive formula variable to subsets of $M \times L$. The LWS-semantics of $\mathcal {L}^w$ basic formulas is defined inductively as follows.

$\mathcal {W},(m,l),\rho \models \top$—always;

$\mathcal {W},(m,l),\rho \models \bot$—never;

$\mathcal {W},(m,l),\rho \models x\bowtie r$ iff $l(x)\bowtie r$;

$\mathcal {W},(m,l),\rho \models \phi _1\wedge \phi _2$ iff $\mathcal {W},(m,l),\rho \models \phi _i, i=1,2$;

$\mathcal {W},(m,l),\rho \models \phi _1\vee \phi _2$ iff $\mathcal {W},(m,l),\rho \models \phi _i, i=1$ or 2;

$\mathcal {W},(m,l),\rho \models [{a}]\phi$ iff for arbitrary $(m',l')\in M\times L$ such that $(m,l)\rightarrow _{a}(m',l')$, we have $\mathcal {W},(m',l'),\rho \models \phi$;

$\mathcal {W},(m,l),\rho \models \langle a\rangle \phi$ iff there exists $(m',l')\in M\times L$ such that $(m,l)\rightarrow _{a}(m',l')$ and $\mathcal {W},(m',l'),\rho \models \phi$;

$\mathcal {W},(m,l),\rho \models X$ iff $(m,l)\in \rho (X)$.

Definition 5

(Syntax of Maximal Equation Blocks) Let ${\mathcal {X}}=\{X_1,\ldots ,X_n\}$ be a set of recursive formula variables. A maximal equation block B is a list of (mutually recursive) equations:

$$\begin{aligned} \begin{array}{lll} X_1&{}=&{}\phi _1\\ &{}\vdots &{}\\ X_n&{}=&{}\phi _n \end{array} \end{aligned}$$

in which $X_i$ are pairwise distinct over ${\mathcal {X}}$ and $\phi _i$ are basic formulas over ${\mathcal {X}}$, for all $i=1,\ldots ,n$.

Each maximal equation block B defines an environment for the recursive formula variables $X_1,\ldots ,X_n$, which is the weakest property that the variables satisfy.

We say that an arbitrary formula $\phi$ is closed with respect to a maximal equation block B if all the recursive formula variables appearing in $\phi$ are defined in B by some of its equations. If all the formulas $\phi _i$ that appears in the right hand side of some equation in B are closed with respect to B, we say that B is closed.

Given an environment $\rho$ and $\overline{\Upsilon }=\langle \Upsilon _1,\ldots ,\Upsilon _n\rangle \in (2^{ M \times L})^n$, let

$$\begin{aligned} \rho _{\overline{\Upsilon }}=\rho [X_1\mapsto \Upsilon _1, \ldots ,X_n\mapsto \Upsilon _n] \end{aligned}$$

be the environment obtained from $\rho$ by updating the binding of $X_i$ to $\Upsilon _i$.

Given a maximal equation block B and an environment $\rho$, consider the function

$$\begin{aligned} f_B^{\rho }: (2^{ M \times L})^n\longrightarrow (2^{ M \times L})^n \end{aligned}$$

defined as follows:

$$\begin{aligned} f_B^\rho (\overline{\Upsilon })=\langle \llbracket {\phi _{1}} \rrbracket {\rho _{\overline{\Upsilon }}},\ldots ,\llbracket \phi _n\rrbracket {\rho _{\overline{\Upsilon }}}\rangle , \end{aligned}$$

where $\llbracket \phi \rrbracket {\rho }=\{(m,l)\in M \times L\mid \mathcal {W},(m,l),\rho \models \phi \}$.

Observe that $(2^{ M \times L})^n$ forms a complete lattice with the ordering, join and meet operations defined as the point-wise extensions of the set-theoretic inclusion, union and intersection, respectively. Moreover, for any maximal equation block B and environment $\rho , f_B^\rho$ is monotonic with respect to the order of the lattice, and therefore, according to the Tarski fixed point theorem (Tarski 1955), it has a greatest fixed point that we denote by $\nu \overline{X}.f_B^\rho$. This fixed point can be characterized as follows:

$$\begin{aligned} \nu \overline{X}.f_B^\rho =\bigcup \{\overline{\Upsilon } \mid \overline{\Upsilon }\subseteq f_B^\rho (\overline{\Upsilon })\}. \end{aligned}$$

Consequently, a maximal equation block defines an environment that satisfies all its equations, i.e.

$$\begin{aligned} \llbracket B\rrbracket \rho =\nu \overline{X}.f_B^\rho . \end{aligned}$$

When B is closed, i.e. there is no free recursive formula variable in B, it is not difficult to see that for any $\rho$ and $\rho ', \llbracket B\rrbracket \rho =\llbracket B\rrbracket \rho '$. So, we just take $\rho =0$ and write $\llbracket B\rrbracket$ instead of $\llbracket B\rrbracket 0$. In the rest of the paper, we will only discuss this kind of equation blocks. (For those that are not closed, we only need to have the initial environment which maps the free recursive variables to subsets of $M \times L$.)

Now we are ready to define the general semantics of $\mathcal {L}^w$: for an arbitrary LWS $\mathcal {W}=( M,{\mathcal {K}},\Sigma ,\theta )$ with $m\in M$, an arbitrary resource valuation $l\in L$ and arbitrary $\mathcal {L}^w$-formula $\phi$ closed w.r.t. a maximal equation block B,

$$\begin{aligned} \mathcal {W},(m,l)\models _B\phi ~\text { iff }~\mathcal {W},(m,l),\llbracket B\rrbracket \models \phi . \end{aligned}$$

The symbol $\models _B$ is interpreted as satisfiability for the block B. Whenever it is not the case that $\mathcal {W},(m,l)\models _B\phi$, we write $\mathcal {W},(m,l)\not \models _B\phi$. We say that a formula $\phi$ is B-satisfiable if there exists at least one LWS that satisfies it for the block B in one of its states under at least one resource valuation; $\phi$ is a B-validity if it is satisfied in all states of any LWS under any resource valuation—in this case, we write $\models _B\phi$.

To exemplify the expressiveness of $\mathcal {L}^w$, we propose the following example of a system with recursively defined properties.

Example 3

Consider a system which only has one type of resource, e.g. energy. It involves three actions: a, b and c, to which three resource-variables $x_a,x_b$ and $x_c$ are associated, respectively. Those resource-variables are used to measure the amount of energy in the system. The specifications of the system are as follows:

• 1. The system cannot cost one or more than one unit of energy;

• 2. The system has the following (action) trace: $abcbcbc\ldots$, i.e. it does an a-action followed by infinitely repeating the sequence bc of actions, during which both b and c will have some nonzero cost.

In our logic, the above-mentioned requirements can be encoded as follows:

$$\begin{aligned} \begin{array}{lll} \phi &{}=&{}\langle a\rangle X,\\ B&{}=&{}\left\{ \begin{array}{lll} X&{}=&{}x_a<1\wedge \langle {b}\rangle (Y\wedge x_c>0),\\ Y&{}=&{}x_a<1\wedge \langle {c}\rangle (X\wedge x_b>0)\end{array}\right\} \end{array} \end{aligned}$$

$\square$

4 Regions and symbolic models

Before proceeding with the definitions of regions and symbolic models, we take a further look at Example 3 in the above section. It is not difficult to see that there exists a model satisfying the formula $\phi$ under the maximal equation block B, but it must be infinite. This is because $x_a$ is synchronized with $x_b$ and $x_c$, which are constantly growing, while $x_a$ is bounded by 1. This example proves that $\mathcal {L}^w$ does not enjoy the finite model property.

In this section, we introduce the region technique for LWS, which is inspired by that for timed automata of Alur and Dill (1990), Alur et al. (1990). It provides an abstract semantics of LWSs in the form of finite labelled transition systems with the truth value of the $\mathcal {L}^w$ formulas being maintained.

Here we introduce the regions defined for a given maximal constant $N\in \mathbb {N}$. For the case where the maximal constant is a rational number $\frac{p}{q}$, where $p,q\in \mathbb {N}$, we only need to get the regions for the maximal constant $p_i$ first and divide all the regions by q. In fact for this case, we could, alternatively, assume that all the constraints involve natural numbers, since the constraints that occur in one formula are finitely many (for instance, we can multiply all the rationals with the same well-chosen integer; by this operation the truth values of the correspondingly modified formulas are preserved).

For $r\in \mathbb {R}_{\ge 0}$, let $\lfloor r\rfloor \overset{\text {def}}{=}\max \{z\in \mathbb {Z}\mid z\le r\}$ denote the integral part of r, and let $\{r\}=r-\lfloor r\rfloor$ denote its fractional part. Moreover, we have $\lceil r\rceil \overset{\text {def}}{=}\min \{z\in \mathbb {Z}\mid z\ge r\}$.

Definition 6

Let $N\in \mathbb {N}$ be a given maximal constant and let ${\mathcal {V}}_i$ be a set of resource-variables for resource $e_i$. Then, $l_i,l_i':{\mathcal {V}}_i\rightarrow \mathbb {R}_{\ge 0}$ are equivalent with respect to N, denoted by $l_i\overset{.}{=}l_i'$ iff:

• 1. $\forall x\in {\mathcal {V}}_i, l_i(x)>N$ iff $l_i'(x)>N$;

• 2. $\forall x\in {\mathcal {V}}_i$ s.t. $0\le l_i(x)\le N$,

  $$\begin{aligned} \lfloor l_i(x)\rfloor =\lfloor l_i'(x)\rfloor \,{\hbox {and}}\,\{l_i(x)\}=0\Leftrightarrow \{l_i'(x)\}=0; \end{aligned}$$

• 3. $\forall x,y\in {\mathcal {V}}_i$ s.t. $0\le l_i(x), l_i(y)\le N$,

  $$\begin{aligned} \{(l_i(x)\}\le \{l_i(y)\}\Leftrightarrow \{(l_i'(x)\}\le \{l_i'(y)\}. \end{aligned}$$

The equivalence classes under $\overset{.}{=}$ are called regions. $[l_i]$ denotes the region which contains the labelling $l_i$ for resource-variables $x\in {\mathcal {V}}_i$ and $R^{{\mathcal {V}}_i}_{N_i}$ denotes the set of all regions for the set ${\mathcal {V}}_i$ of resource-variables for resource $e_i$ and the constant $N_i$. Notice that for a given $N_i\in \mathbb {N}, R^{{\mathcal {V}}_i}_{N_i}$ is finite.

For a region $\delta \in R^{{\mathcal {V}}_i}_{N_i}$, we define the successor region as the region $\delta '$—denoted by $\delta \rightsquigarrow \delta '$—iff:

$$\begin{aligned} \text {for any }l_i\in \delta , \text {there exists}d\in \mathbb {R}_{\ge 0}\text {s.t. }l_i+d\in \delta '. \end{aligned}$$

As we mentioned before, for the case where the maximal constant is a rational number $\frac{p_i}{q_i}$ where $p_i,q_i\in \mathbb {N}$, we only need to get the regions for the maximal constant p first and divide all the regions by $q_i$ to achieve the set of all regions for the set ${\mathcal {V}}_i$ of resource-variables for resource $e_i$ and the constant $\frac{p_i}{q_i}$—denoted by $R^{{\mathcal {V}}_i}_{{p_i}/{q_i}}$. Let

$$\begin{aligned} \begin{array}{l} \mathcal {R}^{\mathcal {V}}=\{\overline{[l]}=([l_1],\ldots ,[l_k])\mid \\ \phantom {\mathcal {R}^{\mathcal {V}}=}[l_i]\in R^{{\mathcal {V}}_i}_{{p_i}/{q_i}},\frac{p_i}{q_i}\in \mathbb {Q}_{\ge 0}\quad \text { for any }i\in \{1,\ldots ,k\}\} \end{array} \end{aligned}$$

For $r\in \mathbb {R}_{\ge 0}$, we use $r\in \overline{[l]}(x)$ to denote $r\in [l_i](x)$, for any $i\in \{1,\ldots ,k\}$ and $x\in {\mathcal {V}}_i$.

We will now define the fundamental concept of a symbolic model of LWS. Every extended state (m, l) is replaced by a so-called extended symbolic state $(m,\overline{[l]})$. Whenever we have transition between two extended states, there should also be a transition between the corresponding symbolic states, i.e.

$$\begin{aligned} (m,\overline{[l]})\rightarrow _{a}(m',\overline{[l']})\text { iff }(m,l)\rightarrow _{a}(m',l'). \end{aligned}$$

Definition 7

Given $\mathcal {R}^{\mathcal {V}}$ and a non-empty set of states $M^s$, a symbolic LWS is a tuple

$$\begin{aligned} \mathcal {W}^s=(\varPi ^s,\Sigma ^s,\theta ^s) \end{aligned}$$

where $\varPi ^s\subseteq M^s\times \mathcal {R}^{\mathcal {V}}$ is a non-empty set of symbolic states $\pi ^s=(m,\overline{\delta }), \Sigma ^s$ is a non-empty set of actions and

$$\begin{aligned} \theta ^s: \varPi ^s\times (\Sigma ^s)\rightarrow 2^{\varPi ^s} \end{aligned}$$

is the symbolic labelled transition function, which satisfies the following:

$$\begin{aligned} \text {if }(m',\overline{\delta '})\in \theta ((m,\overline{\delta }),a)\text {, then }\overline{\delta }\rightsquigarrow \overline{\delta '}. \end{aligned}$$

Given a symbolic LWS, we can define the symbolic satisfiability relation $\models ^s$ with $\pi =(m,\overline{\delta })\in \varPi ^s$ as follows:

$\mathcal {W}^s,\pi ,\rho ^s\models ^s\top$—always;

$\mathcal {W}^s,\pi ,\rho ^s\models ^s\bot$—never;

$\mathcal {W}^s,\pi ,\rho ^s\models ^s x\bowtie r$ iff for any $w\in \overline{\delta }(x), w\bowtie r$;

$\mathcal {W}^s,\pi ,\rho ^s\models ^s\phi _1\wedge \phi _2$ iff $\mathcal {W}^s,\pi ,\rho ^s\models ^s\phi _i, i=1,2$

$\mathcal {W}^s,\pi ,\rho \models ^s\phi _1\vee \phi _2$ iff $\mathcal {W}^s,\pi ,\rho ^s\models ^s\phi _i, i=1$ or 2;

$\mathcal {W}^s,\pi ,\rho ^s\models ^s[{a}]\phi$ iff for any $\pi '\in \varPi ^s$ s.t. $\pi \rightarrow _a\pi '$, we have $\mathcal {W}^s,\pi ',\rho ^s\models ^s\phi$;

$\mathcal {W}^s,\pi ,\rho ^s\models ^s\langle a\rangle \phi$ iff there exists $\pi '\in \varPi ^s$ s.t. $\pi \rightarrow _{a}\pi '$ and $\mathcal {W}^s,\pi ',\rho ^s\models ^s\phi$;

$\mathcal {W}^s,\pi ,\rho ^s\models ^s X$ iff $m\in \rho ^s(X)$,

where $\overline{\delta }[{\mathcal {V}}_a\mapsto 0]$ is defined as:

$$\begin{aligned} \begin{array}{lll} \overline{\delta }[{\mathcal {V}}_a\mapsto 0](x)&{}=&{}\left\{ \begin{array}{llll} 0,&{}&{}&{}x\in {\mathcal {V}}_a\\ \overline{\delta }(x),&{}&{}&{}\text {otherwise} \end{array}\right. \end{array} \end{aligned}$$

Similarly, we can define the symbolic B-satisfiability relation $\models ^s_B$ as in Sect. 3:

$$\begin{aligned} \mathcal {W}^s,\pi \models ^s_B\phi ~\text { iff }~\mathcal {W}^s,\pi ,\llbracket B\rrbracket \models ^s\phi . \end{aligned}$$

Lemma 1

Let $\phi$ be a $\mathcal {L}^w$ formula closed w.r.t a maximal equation block B. If it is satisfied by a symbolic LWS $\mathcal {W}^s=(\varPi ^s,\Sigma ^s,\theta ^s)$ i.e. $\mathcal {W}^s,\pi \models ^s_B\phi$ with $\pi =(m,\overline{\delta })\in \varPi ^s$, then there exists an LWS $\mathcal {W}=(M,{\mathcal {K}},\Sigma ,\theta )$ and a resource valuation $l\in L$ such that $\mathcal {W},(m,l)\models _B\phi$ with $m\in M$.

Proof

Let $\Sigma =\Sigma ^s, {\mathcal {K}}$ be the set of the resources appearing in $\mathcal {R}^{\mathcal {V}}$ and $l\in \overline{\delta }$. The transition function is defined as: $(m_1,\overline{\delta _1},l_1)\xrightarrow {{\overline{u}}}_{a} (m_2,\overline{\delta _2},l_2)$ iff,

• 1. $(m_1,\overline{\delta _1})\rightarrow _{a}(m_2,\overline{\delta _2})$,

• 2. for $i=1,2, l_i\in \overline{\delta _i}$,

• 3. and $l_2=(l_1+{\overline{u}})[{\mathcal {V}}_a\mapsto 0].$

We define the transition relation starting from $(m,\overline{\delta },l)$. Let M be the set of all the states in the form of $(m',\overline{\delta '},l')$ defined for the transitions as the above. Note that it might be infinite. It is easy to verify that $\mathcal {W},((m,\overline{\delta },l),l)\models _B\phi$. $\square$

5 Satisfiability of $\mathcal {L}^w$

In this section, we prove that it is decidable whether a given $\mathcal {L}^w$ formula $\phi$ which is closed w.r.t. a maximal equation block B is satisfiable. We also present a decision procedure for the satisfiability problem of $\mathcal {L}^w$. The results rely on a syntactic characterization of satisfiability that involves a notion of mutually consistent sets that we define later.

Consider an arbitrary formula $\phi \in \mathcal {L}^w$ which is closed w.r.t. a maximal equation block B. In this context, we define the following notions:

• Let $\Sigma [\phi ,B]$ be the set of all actions $a\in \Sigma$ such that a appears in some transition modality of type $\langle {a}\rangle$ or $[{a}]$ in $\phi$ or B.

• For any $e_i\in {\mathcal {K}}$ and $x\in {\mathcal {V}}_i$, let $Q_i[\phi ,B]\subseteq \mathbb {Q}_{\ge 0}$ be the set of all $r\in \mathbb {Q}_{\ge 0}$ such that r is in the label of some state or transition modality of type $x\bowtie r$ that appears in the syntax of $\phi$ or B.

• We denoted by $g_i$ the granularity of $e_i$ in $\phi$, defined as the least common denominator of the elements of $Q_i[\phi ,B]$. Let $R^{{\mathcal {V}}_i}_{{p_i}/{g_i}}[\phi ,B]$ be the set of all regions for resource $e_i$, where $\frac{p_i}{g_i}=\max Q_i[\phi ,B]$. Let

  $$\begin{aligned} \begin{array}{l} \mathcal {R}^{\mathcal {V}}[\phi ,B]=\{\overline{\delta }=(\delta _1,\ldots ,\delta _k) \mid \\ \phantom {\mathcal {R}^{\mathcal {V}}[\phi ,B]}\delta _i\in R^{{\mathcal {V}}_i}_{{p_i}/{g_i}}[\phi ,B]\quad \text { for any }i\in \{1,\ldots ,k\}\}. \end{array} \end{aligned}$$

Observe that $\Sigma [\phi ,B], Q_i[\phi ,B], R^{{\mathcal {V}}_i}_{{p_i}/{g_i}}[\phi ,B]$ and $\mathcal {R}^{\mathcal {V}}[\phi ,B]$ are all finite (or empty).

At this point, we can start our model construction. We fix a formula ${\phi _0}\in \mathcal {L}^w$ that is closed w.r.t. a given maximal equation block B, and supposing that the formula admits a model, we construct a model for it. Let

$$\begin{aligned} \begin{array}{l} \mathcal {L}[{\phi _0},B]=\{\phi \in \mathcal {L}^w\mid \\ \phantom {\mathcal {L}[{\phi _0},B]}\Sigma [\phi ,B]\subseteq \Sigma [\phi _0,B], Q_i[\phi ,B]\subseteq Q_i[\phi _0,B]\}. \end{array} \end{aligned}$$

Here, we are going to construct a symbolic model first. To construct the symbolic model, we will use as symbolic states tuples of type $(\varGamma ,\overline{\delta })\in 2^{\mathcal {L}[{\phi _0},B]}\times \mathcal {R}^{\mathcal {V}}[{\phi _0},B]$, which are required to be maximal in a precise way. The intuition is that a state $(\varGamma ,\overline{\delta })\subseteq 2^{\mathcal {L}[{\phi _0},B]}\times \mathcal {R}^{\mathcal {V}}[{\phi _0},B]$ shall symbolically satisfy the formula $\phi$ in our model, whenever $\phi \in \varGamma$. From this symbolic model, we can generalize an LWS—might be infinite—which is a model of the given $\mathcal {L}^w$ formula. Our construction is inspired from the region construction proposed in (Laroussinie et al. 1995) for timed automata, which adapts of the classical filtration-based model construction used in modal logics (Hughes and Cresswell 1996; Harel et al. 2001; Walukiewicz 2000).

Let $\varOmega [\phi _0,B]\subseteq 2^{\mathcal {L}[{\phi _0},B]}\times \mathcal {R}^{\mathcal {V}}[{\phi _0},B]$. Since $\mathcal {L}[\phi _0,B]$ and $\mathcal {R}^{\mathcal {V}}[{\phi _0},B]$ are both finite, $\varOmega [\phi _0,B]$ is finite.

Definition 8

(Maximal Pair of $\mathcal {L}^w$) For any $(\varGamma ,\overline{\delta })\in \varOmega [\phi _0,B], (\varGamma ,\overline{\delta })$ is said to be maximal iff:

• 1. $\top \in \varGamma , \bot \not \in \varGamma$;

• 2. $x\bowtie r\in \varGamma$ iff for any $w\in \mathbb {R}_{\ge 0}$ s.t. $w\in \overline{\delta }(x), w\bowtie r$;

• 3. $\phi \wedge \psi \in \varGamma$ implies $\phi \in \varGamma$ and $\psi \in \varGamma$;

  $\phi \vee \psi \in \varGamma$ implies $\phi \in \varGamma$ or $\psi \in \varGamma$;

• 4. $X\in \varGamma$ implies $\phi \in \varGamma$, for $X=\phi \in B$.

The following definition establishes the framework on which we will define our model.

Definition 9

(Mutually Consistent Set of $\mathcal {L}^w$ ) Let ${\mathcal {C}}\subseteq 2^{\varOmega [\phi _0,B]}$. $\mathcal {C}$ is said to be mutually consistent if for any $(\varGamma ,\overline{\delta })\in \mathcal {C}$, whenever $\langle a\rangle \psi \in \varGamma$, then there exists $(\varGamma ',\overline{\delta '})\in \mathcal {C}$ s.t.:

• 1. there exists $\overline{\delta ''}$ s.t. $\overline{\delta } \rightsquigarrow \overline{\delta ''}$ and $\overline{\delta '}=\overline{\delta ''}[{\mathcal {V}}_a\mapsto 0]$;

• 2. $\psi \in \varGamma '$;

• 3. for any $[a]\psi '\in \varGamma , \psi '\in \varGamma '$.

We say that $(\varGamma ,\overline{\delta })$ is consistent if it belongs to some mutually consistent set.

The following lemma proves a necessary precondition for the model construction.

Lemma 2

Let $\phi \in \mathcal {L}^w$ be a formula closed w.r.t. a maximal equation block B. Then, $\phi$ is satisfiable iff there exist $\varGamma \subseteq \mathcal {L}[\phi _0,B]$ and $\overline{\delta }\in \mathcal {R}^{\mathcal {V}}[\phi _0,B]$ s.t.

$$\begin{aligned} (\varGamma ,\overline{\delta })\text { is consistent and }\phi \in \varGamma . \end{aligned}$$

Proof

$(\Longrightarrow )$: Suppose $\phi$ is satisfied in the LWS

$$\begin{aligned} \mathcal {W}=( M ,\Sigma ,{\mathcal {K}},\theta ) \end{aligned}$$

under the resource valuation $l\in L$, i.e. there exists $m\in M$ s.t. $\mathcal {W},(m,l)\models _B\phi$. We construct

$$\begin{aligned} \begin{array}{l} \mathcal {C}=\{(\varGamma ,\overline{\delta })\in \varOmega [\phi _0,B]\mid \\ \phantom {\mathcal {C}}\exists m\in M\text { s.t. for any }\psi \in \varGamma ,\exists l\in \overline{\delta }\text { s.t. }\mathcal {W},(m,l)\models _B\psi \}. \end{array} \end{aligned}$$

It is not difficult to verify that $\mathcal {C}$ is a mutually consistent set.

$(\Longleftarrow )$: Let $\mathcal {C}$ be a mutually consistent set.

We construct a symbolic LWS

$$\begin{aligned} \mathcal {W}^s=(\varPi ^s,\Sigma ^s,\theta ^s), \end{aligned}$$

where $\varPi ^s=\mathcal {C}, \Sigma ^s=\Sigma [\phi _0,B]$ and for $(\varGamma ,\overline{\delta }),(\varGamma ',\overline{\delta '})\in \mathcal {C}$, the transition relation $(\varGamma ,\overline{\delta })\xrightarrow {}_{a}(\varGamma ',\overline{\delta '})$ is defined iff

• 1. there exists $\overline{\delta ''}$ s.t. $\overline{\delta } \rightsquigarrow \overline{\delta ''}$ and $\overline{\delta '}=\overline{\delta ''}[{\mathcal {V}}_a\mapsto 0]$;

• 2. whenever $[a]\psi \in \varGamma$ then $\psi '\in \varGamma '$.

Let $\rho ^s(X)=\{(\varGamma ,\overline{\delta })\mid {X\in \varGamma }\}$ for $X\in {\mathcal X}.$

With this construction, we can prove the following implication by a simple induction on the structure of $\phi$, where $(\varGamma ,\overline{\delta })\in \varPi ^s$:

$$\begin{aligned} \phi \in \varGamma \text { implies }\mathcal {W}^s,(\varGamma ,\overline{\delta }),\rho ^s\models ^s\phi . \end{aligned}$$

We prove that $\rho ^s$ is a fixed point of B under the assumption that $X=\phi _X\in B$ as follows:

• $\varGamma \in \rho ^s(X)$ implies $(X,\overline{\delta })\in \varGamma$ by the construction of $\rho ^s$, which implies $(\phi _X,\overline{\delta })\in \varGamma$ by the definition of $\varOmega [\phi _0,B]$.

• Then, $\mathcal {W}^s,\varGamma ,\rho ^s\models ^s\phi _X$ by the implication we just proved.

Thus, $\rho ^s$ is a fixed point of B. Since $\llbracket B\rrbracket$ is the maximal fixed point, $\rho ^s\subseteq \llbracket B\rrbracket$.

Therefore, for any $(\phi ,\overline{\delta })\in \varGamma \in \mathcal {C}$, we have $\mathcal {W}^s,(\varGamma ,\overline{\delta }),\rho ^s\models ^s\phi$, which implies $\mathcal {W}^s,(\varGamma ,\overline{\delta }),\llbracket B\rrbracket \models ^s\phi$ because $\rho ^s\subseteq \llbracket B\rrbracket$.

Hence, $\phi \in \varGamma$ and $(\varGamma ,\overline{\delta })\in \mathcal {C}$ implies $\mathcal {W}^s,\varGamma \models ^s_B\phi$.

By Lemma 1, there exists an LWS $\mathcal {W}=(M,{\mathcal {K}},\Sigma ,\theta )$ and a resource valuation $l\in L$ such that $\mathcal {W},(m,l)\models _B\phi$ with $m\in M$. $\square$

To summarize, the above lemmas allow us to conclude the model constructions.

Theorem 1

For any satisfiable $\mathcal {L}^w$ formula $\phi$ closed w.r.t. a maximal equation block B, there exists a finite symbolic LWS $\mathcal {W}^s=(\varPi ^s,\Sigma ^s,\theta ^s)$ such that $\mathcal {W}^s,\pi \models ^s_B\phi$ for some $\pi \in \varPi ^s$. Reversely, if a $\mathcal {L}^w$ formula $\phi$ is satisfied by a symbolic model, then it is satisfiable, i.e. there exists an LWS $\mathcal {W}=(M,{\mathcal {K}},\Sigma ,\theta )$ and a resource valuation $l\in L$ such that $\mathcal {W},(m,l)\models _B\phi$ for some $m\in M$.

Lemma 2 and Theorem 1 provide a decision procedure for the satisfiability problem of $\mathcal {L}^w$. Given a $\mathcal {L}^w$ formula $\phi _0$ closed w.r.t. a maximal equation block B, the algorithm constructs the model

$$\begin{aligned} \mathcal {W}=({M},{\mathcal {K}},\Sigma ,\theta ). \end{aligned}$$

To do this, we first construct the symbolic LWS

$$\begin{aligned} \mathcal {W}^s=(\varPi ^s,\Sigma ^s,\theta ^s) \end{aligned}$$

with $\phi _0$ being satisfied in some state $\pi \in \varPi ^s$, i.e. $\mathcal {W}^s,\pi \models ^s_B\phi _0$, where $\Sigma ^s=\Sigma [\phi _0,B]$.

If $\phi _0$ is satisfiable, then it is contained in some maximal set $\varGamma$, where $(\varGamma ,\overline{\delta })$ is consistent with $\overline{\delta }\in \mathcal {R}^{\mathcal {V}}[\phi _0,B]$. Hence, $\phi _0$ will be satisfied at some state $\pi$ of $\mathcal {W}^s$. If $\phi _0$ is not satisfiable, then the attempt to construct a model will fail; in this case, the algorithm will halt and report the failure.

We start with a superset of the set of states of $\mathcal {W}$ and then repeatedly delete states when we discover some inconsistency. This will give a sequence of approximations

$$\begin{aligned} \mathcal {W}_0^s\supseteq \mathcal {W}_1^s\supseteq \mathcal {W}_2^s\supseteq \ldots \end{aligned}$$

converging to $\mathcal {W}^s$.

The domains $\varPi ^s_i, i=0,1,2,\ldots$, of these structures are defined below, and they are s.t.

$$\begin{aligned} \varPi ^s_0\supseteq \varPi ^s_1\supseteq \varPi ^s_2\supseteq \ldots . \end{aligned}$$

The transition relation for $\mathcal {W}^s_i$ is defined as follows: for any $(\varGamma ,\overline{\delta }),(\varGamma ',\overline{\delta '})\in \varPi ^s_i, (\varGamma ,\overline{\delta })\xrightarrow {}_{a}(\varGamma ',\overline{\delta '})$ iff

• 1. there exists $\overline{\delta ''}$ s.t. $\overline{\delta } \rightsquigarrow \overline{\delta ''}$ and $\overline{\delta '}=\overline{\delta ''}[{\mathcal {V}}_a\mapsto 0]$;

• 2. whenever $[a]\psi \in \varGamma$, $\psi \in \varGamma '$.

The following is the algorithm for constructing the domains $\varPi ^s_i$ of $\mathcal {W}^s_i$.

Algorithm

• Step 1: Construct $\varPi ^s_0=\varOmega [\phi _0,B]$.

• Step 2: Repeat the following for $i=0,1,2,\ldots$ until no more states are deleted. Find a formula $[{a}]\phi \in \mathcal {L}[{\phi _0},B]$ and a state $(\varGamma ,\overline{\delta })\in \varPi ^s_i$ violating the following property

  $$\begin{aligned} \begin{array}{l} [\forall (\varGamma ',\overline{\delta '})\in \varPi ^s_i,(\varGamma ,\overline{\delta })\xrightarrow {}_{a}(\varGamma ',\overline{\delta '})\ \Rightarrow \phi \in \varGamma ']\\ \text {implies }[a]\phi \in \varGamma . \end{array} \end{aligned}$$

  That is, there exists $\langle a\rangle \lnot \phi \in \varGamma$, but for no $\varGamma '$ and $\overline{\delta '}$ such that $(\varGamma ,\overline{\delta })\xrightarrow {}_{a}(\varGamma ',\overline{\delta '})$, it is the case that $\lnot \phi \in \varGamma '$. Pick such an $[a]\phi$ and $(\varGamma ,\overline{\delta })$. Delete $(\varGamma ,\overline{\delta })$ from $\varPi ^s_i$ to get $\varPi ^s_{i+1}$.

Step 2 can be justified intuitively as follows. To say that $(\varGamma ,\overline{\delta })$ violates the above-mentioned condition, it means that $(\varGamma ,\overline{\delta })$ requires an a-transition to some state that does not satisfy $\phi$; however, the left-hand side of the condition above guarantees that all the outcomes of an a-transition satisfy $\phi$. This demonstrates that $(\varGamma ,\overline{\delta })$ cannot be in $\varPi ^s$, since every state $(\varGamma ,\overline{\delta })$ in $\varPi ^s$ satisfies $\psi$, whenever $\psi \in \varGamma$.

The algorithm must terminate, since there are only finitely many states initially, and at least one state must be deleted during each iteration of step 2 in order to continue. Then, $\phi$ is satisfiable if and only if upon termination there exists $(\varGamma ,\overline{\delta })\in \varPi ^s$ such that $\phi \in \varGamma$. Obviously, $\varPi ^s$ is a mutually consistent set upon termination.

The correctness of this algorithm follows from the proof of Lemma 2. The direction $(\Leftarrow )$ of the proof guarantees that all formulas in any $\varGamma$ with $(\varGamma ,\overline{\delta })\in \varPi ^s$ are satisfiable. The direction $(\Rightarrow )$ of the proof guarantees that all satisfiable $\varGamma$ will not be deleted from $\varPi ^s$.

After we get the symbolic LWS $\mathcal {W}^s$, we can use the technique in Lemma 1 to generalize an LWS $\mathcal {W}=({M},{\mathcal {K}},\Sigma ,\theta ),$ which might be infinite.

Suppose $\phi$ is satisfied by $(\varGamma ,\overline{\delta })\in \varPi ^s$, i.e. $\mathcal {W}^s,(\varGamma ,\overline{\delta })\models ^s_B\phi _0$. Let $\Sigma =\Sigma ^s, {\mathcal {K}}$ be the set of the resources appearing in $\mathcal {R}^{\mathcal {V}}[\phi _0,B]$ and $l\in \overline{\delta }$. The transition function is defined as: $(\varGamma _1,\overline{\delta _1},l_1)\xrightarrow {{\overline{u}}}_{a}(\varGamma _2, \overline{\delta _2},l_2)$ iff,

• 1. $\varGamma _1,\overline{\delta _1})\xrightarrow {}_{a}(\varGamma _2, \overline{\delta _2})$,

• 2. for $i=1,2, l_i\in \overline{\delta _i}$,

• 3. and $l_2=(l_1+{\overline{u}})[{\mathcal {V}}_a\mapsto 0].$

We define the transition relation starting from $(\varGamma ,\overline{\delta },l)$. Let M be the set of all the states in the form of $(\varGamma ',\overline{\delta '},l')$ defined for the transitions as above. Note that the model defined according to this way might be infinite. It is easy to verify that $\mathcal {W},((\varGamma ,\overline{\delta },l),l)\models _B\phi _0$.

Theorem 1, also supported by the above algorithm, demonstrates the decidability of the B-satisfiability problem for $\mathcal {L}^w$.

Theorem 2

(Decidability of B-satisfiability) For an arbitrary maximal equation block B, the B-satisfiability problem for $\mathcal {L}^w$ is decidable.

Example 4

Now we can discuss the satisfiability of the formula $\phi$ in Example 3.

$$\begin{aligned} \begin{array}{rcl} \phi &{}=&{}\langle a\rangle X,\\ B&{}=&{}\left\{ \begin{array}{rcl} X&{}=&{}x_a<1\wedge \langle {b}\rangle (Y\wedge x_c>0),\\ Y&{}=&{}x_a<1\wedge \langle {c}\rangle (X\wedge x_b>0)\end{array}\right\} \end{array} \end{aligned}$$

In Fig. 3 is the symbolic LWS for the above formula $\phi$ w.r.t B by applying our algorithm. Here, the details of using the algorithm to get the model are not presented, limited by the length of the paper, which is very technical.

$$\begin{aligned} \varGamma _0= & {} \{\phi ,\langle {a}\rangle X\}\\ \varGamma _1= & {} \{X,x_a<1,\langle {b}\rangle (Y\wedge x_c>0)\}\\ \varGamma _2= & {} \{Y,x_c>0,x_a<1,\langle {c}\rangle (X\wedge x_b>0)\}\\ \varGamma _3= & {} \{X,x_b>0,x_a<1,\langle {b}\rangle (Y\wedge x_c>0)\}\\ {\delta _0}= & {} [x_a=x_b=x_c=0]\\ {\delta _1}= & {} [x_a=0,0<x_b=x_c<1]\\ {\delta _2}= & {} [x_b=0,0<x_a=x_c<1]\\ {\delta _3}= & {} [x_b=0,0<x_a<x_c<1]\\ {\delta _4}= & {} [x_c=0,0<x_b<x_a<1]\\ {\delta _5}= & {} [x_b=0,0<x_c<x_a<1] \end{aligned}$$

Fig. 3

Symbolic LWS for $\phi$

From the symbolic model in Fig. 3, one can generate an LWS, which in this case is infinite, where $\phi$ is satisfied in some state of it. In Fig. 4 (on the next page), we show part of this infinite model.

$$\begin{aligned} \begin{array}{lll} l_0=(0,0,0)&{}&{}l_5=(0.2,0,0.3)\\ l_1=(0.1,0.1,0)&{}&{}l_6=(0.5,0.2,0)\\ l_2=(\frac{\pi }{4},\frac{\pi }{4},0)&{}&{}l_7=(0.4,0.2,0)\\ l_3=(0.3,0,0.3)&{}&{}l_8=(0.6,0,0.1)\\ l_4=(\frac{\pi }{4},0,\frac{\pi }{4})&{}&{}l_9=(0.5,0,0.1)\\ \ldots \ldots \end{array} \end{aligned}$$

$\square$

Fig. 4

Generalizing LWS from the symbolic model

6 Extension of $\mathcal {L}^w$

The recursive weighted modal logic $\mathcal {L}^w$ introduced in Sect. 3 can be used to encode various interesting scenarios. However, it is not adequate in the sense that bisimilarity of the models does not coincide with the semantic equivalence induced by the logic over the class of models (Hennessy–Milner property). For example, consider the following two simple systems in Fig. 5 (on the next page). Both of them have one type of resource e and one action a—therefore, only one resource variable $x_a^e$. It is not difficult to see that they cannot be distinguished by any formula or theory (set of formulas) of $\mathcal {L}^w$.

Fig. 5

Counter example of $\mathcal {L}^w$ adequacy

In the following, we introduce the recursive weighted logic $\mathcal {L}^t$, which extends $\mathcal {L}^w$ by allowing resource constraints in the transition modalities. For $\mathcal {L}^t$, the maximal equation blocks are defined similarly to for $\mathcal {L}^w$, on top of a class of basic formulas. We show that $\mathcal {L}^t$ is adequate and that its satisfiability problem is still decidable.

In $\mathcal {L}^t$, the resource-variables are still event related, as in $\mathcal {L}^w$, i.e. after each action, the corresponding resource variables will be reset to zero. The same as $\mathcal {L}^w$, we use ${\mathcal {V}}_i=\{x_a^{i}\mid a\in \Sigma \}$ to denote the set of the resource-variables associated for the type of resource $e_i, {\mathcal {V}}_a=\{x_a^{i}\mid i=1,\ldots ,k\}$ to denote the set of the resource-variables associated with the action a and ${\mathcal {V}}=\bigcup _{i=1,\ldots ,k}{\mathcal {V}}_i=\bigcup _{a\in \Sigma }{\mathcal {V}}_a$ to denote the set of all the resource-variables.

Definition 10

(Syntax of $\mathcal {L}^t$ Basic Formulas) For arbitrary $r\in {\mathbb {Q}_{\ge 0}}, a\in \Sigma , x\in {\mathcal {V}}, \bowtie \ \in \{\le ,\ge ,<,>\}, I\subseteq \{1,\ldots ,k\}$ and $X\in {\mathcal {X}}$, let

$$\begin{aligned} \begin{array}{l} \mathcal {L}^t:~~~\phi ^t:=~\top ~|~\bot ~|~x\bowtie r~|~\phi ^t\wedge \phi ^t~|~\phi ^t\vee \phi ^t\\ \phantom {\mathcal {L}^t:~~~\phi ^t}|~[\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t~|~\langle \bigwedge _{i\in I}(e_i\bowtie r_i)\rangle _a\phi ^t~|~X~. \end{array} \end{aligned}$$

The semantics of $\mathcal {L}^t$ basic formulas is defined similar to $\mathcal {L}^w$ except for that of the transition modalities, which are defined as follows:

$\mathcal {W},(m,l),\rho \models ^t[\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t$ iff for arbitrary $(m',l')\in M\times L$ such that $(m,l)\xrightarrow {}_{a}(m',l')$ and $(l'-l)(e_i)\bowtie r_i$ for any $i\in I$, we have $\mathcal {W},(m',l'[{\mathcal {V}}_a\mapsto 0]),\rho \models ^t\phi ^t$,

$\mathcal {W},(m,l),\rho \models ^t\langle \bigwedge _{i\in I}(e_i\bowtie r_i)\rangle _a\phi ^t$ iff there exists $(m',l')\in M\times L$ such that $(m,l)\xrightarrow {}_{a}(m',l')$,$(l'-l)(e_i)\bowtie r_i$ for any $i\in I$ and $\mathcal {W},(m',l'[{\mathcal {V}}_a\mapsto 0]),\rho \models ^t\phi ^t$.

As for $\mathcal {L}^w$, we can define the semantics of $\mathcal {L}^t$ with maximal equation blocks $B^t$:

$$\begin{aligned} \mathcal {W},(m,l)\models _{B^t}\phi ^t\text { iff }\mathcal {W},(m,l), \llbracket {B^t}\rrbracket \models ^t\phi ^t. \end{aligned}$$

6.1 Adequacy of $\mathcal {L}^t$

It is clear that $\mathcal {L}^t$ is more expressive than $\mathcal {L}^w$. We will show in the following that $\mathcal {L}^t$ is sufficiently expressive to characterize weighted bisimilarity, i.e. $\mathcal {L}^t$ enjoys the Hennessy–Milner property. We do this by proving that the logic without fixed points is already adequate. Since we do not consider the fixed points, the environment is not necessary for the semantics. So, in the following lemma, we only write $\models$ instead of $\models _{B^t}$ and we use $\mathcal {L}^t/X$ to denote $\mathcal {L}^t$ without fixed points.

Lemma 3

Let $\mathcal {W}=( M ,{\mathcal {K}},\Sigma ,\theta )$ be an image-finite labelled weighted transition system. Then, for any $m,m'\in M$:

$$\begin{aligned} \begin{array}{l} m\sim m'~~\text { iff }~~\forall \phi ^t\in \mathcal {L}^t/X\text { and }l\in L\\ \phantom {m\sim m'~~}\mathcal {W},(m,l)\models \phi ^t\Leftrightarrow \mathcal {W},(m',l)\models \phi ^t. \end{array} \end{aligned}$$

Proof

($\Longrightarrow$) Induction on $\phi ^t$.

The cases $\top ,\bot$ and $\phi ^t\wedge \psi ^t,\phi ^t\vee \psi ^t$ are easy.

• Case $x \bowtie r$:

  $\mathcal {W},(m,l)\models x\bowtie r$ implies $l(x)\bowtie r$, which implies

  $\mathcal {W},(m',l)\models x\bowtie r$.

  Hence, $\mathcal {W},(m,l)\models x\bowtie r$ implies $\mathcal {W},(m',l)\models x\bowtie r$.

  Similarly $\mathcal {W},(m',l)\models x\bowtie r$ implies $\mathcal {W},(m,l)\models x\bowtie r$.

• Case $[\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t$:

  $\mathcal {W},(m,l)\models [\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t$ implies:

  for any $(m_1,l_1)\in M \times L$ s.t.

  • 1. $(m,l)\xrightarrow {}_{a}(m_1,l_1)$ and

  • 2. $(l_1-l)(e_i)\bowtie r_i$ for any $i\in I$,

  then $\mathcal {W},(m_1,l_1)\models \phi ^t$.

  $(m,l)\xrightarrow {}_{a}(m_1,l_1)$ implies $m\xrightarrow {{\overline{u}}}_{a}m_1$ and $l_1=l+{\overline{u}}$.

  Since $m\sim m'$, for any $m_1'\in M$ s.t. $m'\xrightarrow {{\overline{u}}}_{a}m_1'$, there exists $m_1\in M$ s.t. $m\xrightarrow {{\overline{u}}}_{a}m_1$ and $m_1\sim m_1'$.

  By inductive hypothesis,

  $\mathcal {W},(m_1,l_1)\models \phi ^t$ implies $\mathcal {W},(m_1',l_1)\models \phi ^t$.

  So for any $(m_1',l_1)\in M$ s.t.

  • 1. $(m',l)\xrightarrow {}_{a}(m_1',l_1)$ and

  • 2. $(l_1-l)(e_i)\bowtie r_i$ for any $i\in I$,

    we have $\mathcal {W},(m_1',l_1)\models \phi ^t$.

    Then, $\mathcal {W},(m',l)\models [\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t$.

    Hence, $\mathcal {W},(m,l)\models [\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t$ implies

    $\mathcal {W},(m',l)\models [\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t$.

    Similarly, $\mathcal {W},(m',l)\models [\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t$ implies

    $\mathcal {W},(m,l)\models [\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t$.

• Case $\langle \bigwedge _{i\in I}(e_i\bowtie r_i)\rangle _a\phi ^t$:

  $\mathcal {W},(m,l)\models \langle \bigwedge _{i\in I}(e_i\bowtie r_i)\rangle _a\phi ^t$ implies:

  there exists $(m_1,l_1)\in M \times L$ s.t.

  • 1. $(m,l)\xrightarrow {}_{a}(m_1,l_1)$,

  • 2. $(l_1-l)(e_i)\bowtie r_i$ for any $i\in I$ and

  • 3. $\mathcal {W},(m_1,l_1)\models \phi ^t$.

    $(m,l)\rightarrow _{a}(m_{1},l_{1})$ implies $m\xrightarrow {{\overline{u}}}_{a}m_1$ and $l_1=l+{\overline{u}}$.

    Since $m\sim m'$, there exists $m_1'$ such that $m'\xrightarrow {{\overline{u}}}_{a}m_1'$ and

    $m_1\sim m_1'$.

    By inductive hypothesis,

    $\mathcal {W},(m_1,l_1)\models \phi ^t$ implies $\mathcal {W},(m_1',l_1)\models \phi ^t$.

  So we have that there exists $(m_1',l_1)\in M \times L$ s.t.

  • 1. $(m',l)\xrightarrow {}_{a}(m_1',l_1)$,

  • 2. $(l_1-l)(e_i)\bowtie r_i$ for any $i\in I$ and

  • 3. $\mathcal {W},(m_1',l_1)\models \phi ^t$.

  Therefore, $\mathcal {W},(m',l)\models \langle \bigwedge _{i\in I}(e_i\bowtie r_i)\rangle _a\phi ^t$.

  Hence, $\mathcal {W},(m,l)\models \langle \bigwedge _{i\in I}(e_i\bowtie r_i)\rangle _a\phi ^t$ implies

  $\mathcal {W},(m',l)\models \langle \bigwedge _{i\in I}(e_i\bowtie r_i)\rangle _a\phi ^t$.

  Similarly, $\mathcal {W},(m',l)\models \langle \bigwedge _{i\in I}(e_i\bowtie r_i)\rangle _a\phi ^t$ implies

  $\mathcal {W},(m,l)\models \langle \bigwedge _{i\in I}(e_i\bowtie r_i)\rangle _a\phi ^t$.

($\Longleftarrow$) Let

$$\begin{aligned} \begin{array}{l} R=\{(m,m')\mid \\ \forall \phi ^t\in \mathcal {L}^t/X,\mathcal {W},(m,l)\models \phi ^t \Leftrightarrow \mathcal {W},(m',l)\models \phi ^t\}. \end{array} \end{aligned}$$

We prove that R is a weighted bisimulation relation.

• If $m\xrightarrow {{\overline{u}}}_{a}m_1$:

  If for any $I\subseteq \{1,\ldots ,k\}$ and for any $i\in I, r_i\in \mathbb Q$ s.t. ${\overline{u}}(e_i)\bowtie r$, there exists no $m_1'\in M$ s.t

  $m'\xrightarrow {{\overline{u}}}_{a}m_1'$ and $\mathcal {W},(m',l)\models [\bigwedge _{i\in I}(e_i\bowtie r)]_a\bot$.

  Then, $\mathcal {W},(m,l)\models [\bigwedge _{i\in I}(e_i\bowtie r)]_a\bot$ since $(m,m')\in R$.

  This contradicts the premise! Hence, there exists at least one $m_1'\in M$ s.t $m'\xrightarrow {{\overline{u}}}_{a}m_1'$.

  Suppose:

  $S=\{m_h'\mid m'\xrightarrow {{\overline{u}}}_{a}m_h'\}$ and $(m_1,m_h')\not \in R$ for any h;,

  i.e. for any h, there exists $l_h$ and $\phi _h^t$ s.t.

  $$\begin{aligned} \mathcal {W},(m_1,l_h)\models \phi _h^t\text {and}\mathcal {W},(m_h',l_h)\not \models \phi _h^t. \end{aligned}$$

  For any h and for any $x_b^i\in {\mathcal {V}}(\phi ^t_h)$ with $b\in \Sigma$ and $i\in \{1,\ldots ,k\}$, we introduce one new action $b_h$ and one new resource variable $x_{b_h}^i$.

  Let ${\phi ^t_h}'=\phi _h^t\{x_{b_h}^i/x_b^i\}$ for every $\phi _h^t$.

  Let $l'(x_{b_h}^i)=l_h(x_b^i)$ for any $x_{b_h}^i$ and $l'(x_a^i)=0$ for any $x_a^i$ with $a\in \Sigma$. Then, for all h, we have:

  $\mathcal {W},(m_1,l')\models \bigwedge _h{\phi _h^t}'$ and $\mathcal {W},(m_h',l')\not \models {\phi _h^t}'$.

  Then, there exists l s.t.

  • 1. $l'=(l+{\overline{u}})[{\mathcal {V}}\mapsto 0]$,

  • 2. $\mathcal {W},(m,l)\models []_a\bigwedge _h{\phi _h^t}'$ and

  • 3. $\mathcal {W},(m',l)\not \models []_a\bigwedge _h{\phi _h^t}'.$ Contradiction!

  Hence, there exists $m_1'\in M$ s.t. $m'\xrightarrow {{\overline{u}}}_{a}m_1'$ and $m_1\sim m_1'$.

• If $m'\xrightarrow {{\overline{u}}}_{a}m_1'$: similar as above.$\square$

Theorem 3

(Adequancy of $\mathcal {L}^t$) Let

$$\begin{aligned} \mathcal {W}=( M ,{\mathcal {K}},\Sigma ,\theta ) \end{aligned}$$

be an image-finite labelled weighted transition system. Then, for any $m,m'\in M$:

$$\begin{aligned} \begin{array}{l} m\sim m'~~\text { iff }\text { for any }\phi ^t\in \mathcal {L}^t\text { under }B^t\text { and }l\in L,\\ \phantom {m\sim m'~~}\mathcal {W},(m,l)\models _{B^t}\phi ^t\Leftrightarrow \mathcal {W},(m',l)\models _{B^t}\phi ^t. \end{array} \end{aligned}$$

6.2 Satisfiability of $\mathcal {L}^t$

We can use a similar technique to the one used in Sect. 5 for checking satisfiability of $\mathcal {L}^w$, to decide the satisfiability of $\mathcal {L}^t$ by adding the requirements of the weights on the transitions. More precisely, we define the symbolic semantics for $\mathcal {L}^t$ and add the requirements of the weights on the transitions and the definitions of maximal pair $(\varGamma ,\overline{\delta })$ and mutually consistent set $\mathcal {C}$ as follows:

$\mathcal {W}^s,\pi ,\rho ^s\models ^s[{\bigwedge _{i\in I}(e_i\bowtie r_i)}]_a\phi$ iff:

for any $\pi '=(m',\overline{\delta '})\in \varPi ^s$ s.t.

• (1) $\pi \rightarrow _a\pi '$ and

• (2) $w'-w\bowtie r_i$ for any $i\in I$ and $w\in \overline{\delta }(e_i),w'\in \overline{\delta '}(e_i)$,

we have $\mathcal {W}^s,\pi ',\rho ^s\models ^s\phi$,

$\mathcal {W}^s,\pi ,\rho ^s\models ^s\langle \bigwedge _{i\in I}(e_i\bowtie r_i)\rangle _a\phi$ iff:

there exists $\pi '=(m',\overline{\delta '})\in \varPi ^s$ s.t.

• (1) $\pi \rightarrow _{a}\pi '$,

• (2) $w'-w\bowtie r_i$ for any $i\in I$ and $w\in \overline{\delta }(e_i),w'\in \overline{\delta '}(e_i)$

  and

• (3) $\mathcal {W}^s,\pi ',\rho ^s\models ^s\phi$.

Definition 11

(Maximal Pair of $\mathcal {L}^t$) For any $(\varGamma ,\overline{\delta })\in \varOmega [\phi ^t_0,B^t], (\varGamma ,\overline{\delta })$ is said to be maximal iff:

• 1. $\top \in \varGamma , \bot \not \in \varGamma$;

• 2. $x\bowtie r\in \varGamma$ iff for any $w\in \mathbb {R}_{\ge 0}$ s.t. $w\in \overline{\delta }(x), w\bowtie r$;

• 3. $\phi \wedge \psi \in \varGamma$ implies $\phi \in \varGamma$ and $\psi \in \varGamma$;

  $\phi \vee \psi \in \varGamma$ implies $\phi \in \varGamma$ or $\psi \in \varGamma$;

• 4. $\langle \bigwedge _{i\in I}e_i<r_i\rangle _a\phi \in \varGamma$ implies $\langle \bigwedge _{i\in I}e_i\le r_i\rangle _a\phi \in \varGamma$,

  $\langle \bigwedge _{i\in I}e_i>r_i\rangle _a\phi \in \varGamma$ implies $\langle \bigwedge _{i\in I}e_i\ge r_i\rangle _a\phi \in \varGamma$;

• 5. $\langle \bigwedge _{i\in I}e_i\le r_i\rangle _a\phi \in \varGamma$ implies $\langle \bigwedge _{i\in I}e_i<r_i+s_i\rangle _a\phi \in \varGamma$,

  $\langle \bigwedge _{i\in I}e_i\ge r_i\rangle _a\phi \in \varGamma$ implies $\langle \bigwedge _{i\in I}e_i>r_i-s_i\rangle _a\phi \in \varGamma$,

  for any $s_i\in \mathbb Q$ and $s_i>0$;

• 6. $X\in \varGamma$ implies $\phi \in \varGamma$, for $X=\phi \in B$.

Definition 12

(Mutually Consistent Set of $\mathcal {L}^t$) Let ${\mathcal {C}}\subseteq 2^{\varOmega [\phi ^t_0,B^t]}$. $\mathcal {C}$ is said to be mutually consistent if for any $(\varGamma ,\overline{\delta })\in \mathcal {C}$, whenever $\langle \bigwedge _{i\in I}(e_i\bowtie r_i)\rangle _a\psi \in \varGamma$, then there exists $(\varGamma ',\overline{\delta '})\in \mathcal {C}$ s.t.:

• 1. there exists $\overline{\delta ''}$ s.t.

  • (1) $\overline{\delta }\rightsquigarrow \overline{\delta ''}$,

  • (2) $\overline{\delta '}=\overline{\delta ''}[{\mathcal {V}}_a\mapsto 0]$ and

  • (3) $w'-w\bowtie r_i$ for any $i\in I$ and $w\in \overline{\delta }(e_i),w'\in \overline{\delta '}(e_i)$;

• 2. $\psi \in \varGamma '$;

• 3. for any $[\bigwedge _{j\in J}(e_j\bowtie r_j)]_a\psi '\in \varGamma$,

  • (1) $w'-w\bowtie r_j$ for any $j\in J$ and $w\in \overline{\delta }(e_j),w'\in \overline{\delta '}(e_j)$ and

  • (2) $\psi '\in \varGamma '$.

Based on the above definitions, we can prove similar lemma and theorem as Lemma 2 and Theorem 1. Therefore, we prove that the satisfiability problem of $\mathcal {L}^t$ is decidable.

Alternatively, one can solve this problem in the following way:

• firstly, encode this problem into a satisfiability problem similar to that of $\mathcal {L}^w$, by translating the given $\mathcal {L}^t$ formula into $\mathcal {L}^w$ with a special 0-cost action;

• secondly, check the satisfiability of the new $\mathcal {L}^w$ formula by using the model construction algorithm of Sect. 5 with a minor modification;

• and thirdly, if the $\mathcal {L}^w$ formula is not satisfiable, then the given $\mathcal {L}^t$ formula is not satisfiable either; otherwise, the given $\mathcal {L}^t$ formula is satisfiable and we can finally generate the model for it according to the model for the corresponding $\mathcal {L}^w$ formula.

In the following, we show how to do this in details.

Firstly, we define the function that translate a $\mathcal {L}^t$ formula into $\mathcal {L}^w$ with a special 0-cost action ($\varepsilon$).

Let $F:\mathcal {L}^t\rightarrow \mathcal {L}^w$ be a function encoding $\mathcal {L}^t$ formulas into $\mathcal {L}^w$ defined inductively. The basic cases are trivial. We only encode the transition modalities as follows, where $\varepsilon$ is a newly introduced action which always cost 0 unit of all types of resources and $x_\varepsilon ^i$ for all $i\in \{1,\ldots ,k\}$ are the newly introduced resource variables:

$$\begin{aligned} F([\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t)= & {} [\varepsilon ][a](\bigwedge _{i\in I}(x_\varepsilon ^i\bowtie r_i)\rightarrow F(\phi ^t)),\\ F(\langle {\bigwedge _{i\in I}(e_i\bowtie r_i)}\rangle _a\phi ^t)= & {} \langle {\varepsilon }\rangle \langle {a}\rangle (\bigwedge _{i\in I}(x_\varepsilon ^i\bowtie r_i)\wedge F(\phi ^t)). \end{aligned}$$

Based on these, we can also extend F to the maximal equation blocks, defined as:

$$\begin{aligned} F(B)=\{X=F(\phi _X)\mid X=\phi _X\in B^t\}. \end{aligned}$$

Lemma 4

Let $\mathcal {W}=(M,{\mathcal {K}},\Sigma ,\theta )$ be an LWS and $\mathcal {W}'=(M,{\mathcal {K}},\Sigma ',\theta ')$ be an LWS extended from $\mathcal {W}$, which is defined by taking

$$\begin{aligned} \Sigma '=\Sigma \cup {\varepsilon },\theta '= \theta \cup \{m\xrightarrow {\overline{0}}_{\varepsilon }m)\mid m\in M\}. \end{aligned}$$

Then, for any $\mathcal {L}^t$ formula $\phi ^t$ closed w.r.t $B^t$, any $m\in M$ and $l\in L$,

$$\begin{aligned} \mathcal {W},(m,l)\models _{B^t}\phi ^t\text { iff }\mathcal {W}',(m,l')\models _B F(\phi ^t), \end{aligned}$$

where $F(\phi ^t)$ is the corresponding $\mathcal {L}^w$ formula closed w.r.t $B=F(B^t)$ and $l':{\mathcal {V}}'={\mathcal {V}}\cup \{x_\varepsilon ^i\mid i\in \{1,\ldots ,k\}\}\rightarrow \mathbb {R}_{\ge 0}$ is a variable valuation satisfying $l'(x)=l(x)$ for any $x\in {\mathcal {V}}$.

Proof

($\Rightarrow$) Induction on the structure of $\phi ^t$.

The basic cases are trivial.

• Case $(\bigwedge _{i\in I}(e_i\bowtie r_i))_a\phi ^t$:

  $\mathcal {W},(m,l)\models _{B^t}[\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t$ implies:

  for any $(m_1,l_1)\in M\times L$ such that

  • 1. $(m,l)\xrightarrow {}_{a}(m_1,l_1)$ and

  • 2. $(l_1-l)(e_i)\bowtie r_i$ for any $i\in I$,

    we have $\mathcal {W},(m_1,l_1[{\mathcal {V}}_a\mapsto 0])\models _{B^t}\phi ^t$.

    By the construction of $\mathcal {W}', m\xrightarrow {\underline{0}}_{\varepsilon }m$, which implies $(m,l')\xrightarrow {}_{\varepsilon }(m,l')$.

  Suppose

  • 1. $(m,l'[{\mathcal {V}}_\varepsilon \mapsto 0])\xrightarrow {}_{a}(m_1,l_1')$ and

  • 2. $l_1'(x_\varepsilon ^i)\bowtie r_i$ for any $i\in I$.

  $(m,l'[{\mathcal {V}}_\varepsilon \mapsto 0])\xrightarrow {}_{a}(m_1,l_1')$ implies

  $m\xrightarrow {{\overline{u}}}_{a}m_1$ and $l_1'-l'[{\mathcal {V}}_\varepsilon \mapsto 0]={\overline{u}}$.

  For any $i\in I, l'[{\mathcal {V}}_\varepsilon \mapsto 0](x_\varepsilon ^i)=0$,

  so $(l_1'-l'[{\mathcal {V}}_\varepsilon \mapsto 0])(e_i)\bowtie r_i$.

  Let $l_1:{\mathcal {V}}\rightarrow \mathbb {R}_{\ge 0}$ be a variable valuation defined as:

  for any $x\in {\mathcal {V}}, l_1(x)=l_1'(x)$.

  Then, $l_1-l={\overline{u}}$ and $(l_1-l)(e_i)\bowtie r_i$ for any $i\in I$.

  Hence, $(m,l)\xrightarrow {}_{a}(m_1,l_1)$ and $(l_1-l)(e_i)\bowtie r_i$ for any $i\in I$, which implies $\mathcal {W},(m_1,l_1[{\mathcal {V}}_a\mapsto 0])\models _{B^t}\phi ^t$. By inductive hypothesis, $\mathcal {W}',(m_1,l_1'[{\mathcal {V}}_a\mapsto 0])\models _{B}F(\phi ^t)$. Hence, $\mathcal {W}',(m,l')\models _B F([\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t)$.

• Case $\langle {\bigwedge _{i\in I}(e_i\bowtie r_i)}\rangle _a\phi ^t$:

  $\mathcal {W},(m,l)\models _{B^t}\langle {\bigwedge _{i\in I}(e_i\bowtie r_i)}\rangle _a\phi ^t$ implies

  there exists $(m_1,l_1)\in M\times L$ such that

  • 1. $(m,l)\xrightarrow {}_{a}(m_1,l_1)$,

  • 2. $(l_1-l)(e_i)\bowtie r_i$ for any $i\in I$ and

  • 3. $\mathcal {W},(m_1,l_1[{\mathcal {V}}_a\mapsto 0])\models _{B^t}\phi ^t$.

  By the construction of $\mathcal {W}', m\xrightarrow {\underline{0}}_{\varepsilon }m$, which implies $(m,l')\xrightarrow {}_{\varepsilon }(m,l')$.

  $(m,l)\xrightarrow {}_{a}(m_1,l_1)$ implies $m\xrightarrow {{\overline{u}}}_{a}m_1$ and $l_1-l={\overline{u}}$.

  Let $l_1':{\mathcal {V}}'\rightarrow \mathbb {R}_{\ge 0}$ be a variable valuation defined as:

  • (1) $l_1'(x)=l_1(x)$ for any $x\in {\mathcal {V}}$ and

  • (2) $l_1'(x_\varepsilon ^i)={\overline{u}}(e_i)$ for any $x_\varepsilon ^i\in {\mathcal {V}}'-{\mathcal {V}}$.

  Then, $l_1'-l'[{\mathcal {V}}_\varepsilon \mapsto 0]={\overline{u}}$.

  So $(m,l'[{\mathcal {V}}_\varepsilon \mapsto 0])\xrightarrow {}_{a}(m_1,l_1')$.

  For any $i\in I, l_1'[{\mathcal {V}}_a\mapsto 0](x_\varepsilon ^i)=l_1'(x_\varepsilon ^i)={\overline{u}}(e_i)$, which implies $l_1'[{\mathcal {V}}_a\mapsto 0](x_\varepsilon ^i)\bowtie r_i$. By inductive hypothesis $\mathcal {W},(m_1,l_1[{\mathcal {V}}_a\mapsto 0])\models _{B^t}\phi ^t$ implies $\mathcal {W}',(m_1,l_1'[{\mathcal {V}}_a\mapsto 0])\models _B F(\phi ^t)$. Hence, $\mathcal {W}',(m_1,l_1'[{\mathcal {V}}_a\mapsto 0])\models _B F(\langle {\bigwedge _{i\in I}(e_i\bowtie r_i)}\rangle _a\phi ^t)$.

($\Leftarrow$) Induction on the structure of $\phi ^t$.

The basic cases are trivial.

• Case $[\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t$:

  By the construction of $\mathcal {W}', m\xrightarrow {\underline{0}}_{\varepsilon }m$, which implies $(m,l')\xrightarrow {}_{\varepsilon }(m,l')$.

  Hence, $\mathcal {W}',(m,l')\models _B F([\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t)$ implies for any $(m_1,l_1')\in M\times L$ such that

  • 1. $(m,l'[{\mathcal {V}}_\varepsilon \mapsto 0])\xrightarrow {}_{a}(m_1,l_1')$ and

  • 2. $l_1'(x_\varepsilon ^i)\bowtie r_i$ for any $i\in I$,

    we have $\mathcal {W}',(m_1,l_1'[{\mathcal {V}}_a\mapsto 0])\models _{B}F(\phi ^t)$.

  Suppose

  • 1. $(m,l)\xrightarrow {}_{a}(m_1,l_1)$ with $l_1-l={\overline{u}}$ and

  • 2. ${\overline{u}}(e_i)\bowtie r_i$ for any $i\in I$.

  $(m,l)\xrightarrow {}_{a}(m_1,l_1)$ with $l_1-l={\overline{u}}$ implies $m\xrightarrow {{\overline{u}}}_{a}m_1$.

  Let $l_1':{\mathcal {V}}'\rightarrow \mathbb {R}_{\ge 0}$ be a variable valuation defined as:

  • (1) $l_1'(x)=l_1(x)$ for any $x\in {\mathcal {V}}$ and

  • (2) $l_1'(x_\varepsilon ^i)={\overline{u}}(e_i)$ for any $x_\varepsilon ^i\in {\mathcal {V}}'-{\mathcal {V}}$.

    Then, $l_1'-l'[{\mathcal {V}}_\varepsilon \mapsto 0]={\overline{u}}$.

    So $(m,l'[{\mathcal {V}}_\varepsilon \mapsto 0])\xrightarrow {}_{a}(m_1,l_1')$.

    And for any $i\in I, l_1'(x_\varepsilon ^i)={\overline{u}}(e_i)\bowtie r_i$.

    So $\mathcal {W}',(m_1,l_1'[{\mathcal {V}}_a\mapsto 0])\models _{B}F(\phi ^t)$. By inductive hypothesis, $\mathcal {W},(m_1,l_1[{\mathcal {V}}_a\mapsto 0])\models _{B^t}\phi ^t$.

    Hene, $\mathcal {W},(m,l')\models _{B^t}[\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t$.

• Case $\langle {\bigwedge _{i\in I}(e_i\bowtie r_i)}\rangle _a\phi ^t$:

  By the construction of $\mathcal {W}', m\xrightarrow {\underline{0}}_{\varepsilon }m$, which implies $(m,l')\xrightarrow {}_{\varepsilon }(m,l')$.

  Hence, $\mathcal {W}',(m_1,l_1'[{\mathcal {V}}_a\mapsto 0])\models _B F(\langle \bigwedge _{i\in I}(e_i\bowtie r_i)\rangle _a\phi ^t)$ implies there exists $(m_1,m_1')\in M\times L$ such that:

  • 1. $(m,l'[{\mathcal {V}}_\varepsilon \mapsto 0])\xrightarrow {}_{a}(m_1,l_1')$,

  • 2. $l_1'[{\mathcal {V}}_a\mapsto 0](x_\varepsilon ^i)\bowtie r_i$ for any $i\in I$

  • 3. and $\mathcal {W}',(m_1,l_1'[{\mathcal {V}}_a\mapsto 0])\models _B F(\phi ^t)$.

  $(m,l'[{\mathcal {V}}_\varepsilon \mapsto 0])\xrightarrow {}_{a}(m_1,l_1')$ implies

  • 1. $m\xrightarrow {{\overline{u}}}_{a}m_1$ and

  • 2. $l_1'-l'[{\mathcal {V}}_\varepsilon \mapsto 0]={\overline{u}}$.

    For any $i\in I$, because $l'[{\mathcal {V}}_\varepsilon \mapsto 0](x_\varepsilon ^i)=0$, so

    $l_1'[{\mathcal {V}}_a\mapsto 0](x_\varepsilon ^i)=l_1'(x_\varepsilon ^i)=(l_1'-l'[{\mathcal {V}}_\varepsilon \mapsto 0])(x_\varepsilon ^i)\bowtie r_i$, which implies ${\overline{u}}(e_i)\bowtie r_i$.

    Let $l_1:{\mathcal {V}}\rightarrow \mathbb {R}_{\ge 0}$ be a variable valuation defined as:

    for any $x\in {\mathcal {V}}, l_1(x)=l_1'(x)$.

    Then, $l_1-l={\overline{u}}$ and $(l_1-l)(e_i)\bowtie r_i$ for any $i\in I$.

    By inductive hypothesis, $\mathcal {W}',(m_1,l_1'[{\mathcal {V}}_a\mapsto 0])\models _B F(\phi ^t)$ implies $\mathcal {W},(m_1,l_1[{\mathcal {V}}_a\mapsto 0])\models _{B^t}\phi ^t$.

    Hence, $\mathcal {W},(m,l)\models _{B^t}\langle {\bigwedge _{i\in I}(e_i\bowtie r_i)}\rangle _a\phi ^t$.$\square$

In the following, we show how to construct the symbolic model of $\phi ^t$. Firstly, we construct a symbolic model for $F(\phi ^t)$ by using the algorithm of $\mathcal {L}^w$ with a minor modification in the definition of mutually consistent set as follows.

Definition 13

($\varepsilon$ Mutually Consistent of $\mathcal {L}^w$) Let ${\mathcal {C}}\subseteq 2^{\varOmega [F(\phi ^t),H(B^t)]}$. $\mathcal {C}$ is said to be $\varepsilon mutually consistent$ if ${\mathcal {C}}$ is mutually consistent (Definition 9) and for any $(\varGamma ,\overline{\delta })\in \mathcal {C}$, whenever $\langle \varepsilon \rangle \psi \in \varGamma$, then there exists $(\varGamma ',\overline{\delta '})\in \mathcal {C}$ s.t.:

• 1. $\overline{\delta '}=\overline{\delta }[{\mathcal {V}}_{\varepsilon }\mapsto 0]$;

• 2. $\psi \in \varGamma '$;

• 3. for any $[\varepsilon ]\psi '\in \varGamma , \psi '\in \varGamma '$.

It is not difficult to prove similar results as the ones stated in Lemma 2 and Theorem 1. If $F(\phi ^t)$ is not satisfiable, then by Lemma 4, $\phi ^t$ is not satisfiable either.

Otherwise, we get a symbolic model $\mathcal {W}^s$ for $F(\phi ^t)$. In the following, we construct a symbolic model for $\phi ^t$ without $\varepsilon$-transitions according to $\mathcal {W}^s$.

Given a symbolic LWS $\mathcal {W}^s=(\varPi ^s,\Sigma ^s,\theta ^s)$ which is constructed according to the definition of $\varepsilon$-mutually consistent set, we generate

$$\begin{aligned} \mathcal {W}^s_t=(\varPi ^s_t,\Sigma ^s_t,\theta ^s_t) \end{aligned}$$

with $\Sigma ^s_t=\Sigma ^s/{\varepsilon }$. $\varPi ^s_t$ and $\theta ^s_t$ are defined according to the following three steps that must be applied, consecutively, in the order they are described:

• 1. as shown in Fig. 6, for any $\pi _1\xrightarrow {0}_{\varepsilon }\pi _2\xrightarrow {0}_{\varepsilon }\pi _3$

  let $\pi '=\{\pi _2,\pi _3\}$ and

  • (1) $\pi '_2\xrightarrow {}_{a}\pi _2$ implies $\pi '_2\xrightarrow {}_{a}\pi ', \pi '_3\xrightarrow {}_{b}\pi _3$ implies $\pi '_3\xrightarrow {}_{b}\pi ', a,b\in \Sigma ^s_t$,

  • (2) $\pi _2\xrightarrow {}_{a}\pi ''_2$ implies $\pi '\xrightarrow {}_{a}\pi ''_2, \pi _3\xrightarrow {}_{b}\pi ''_3$ implies $\pi '\xrightarrow {}_{b}\pi ''_3, a,b\in \Sigma ^s_t$;

• 2. as shown in Fig. 7, for any $\pi _1\xrightarrow {0}_{\varepsilon }\pi _2$

  for any $\pi _1\xrightarrow {}_{a}\pi '_1$, delete this transition, $a,b\in \Sigma ^s_t$;

• 3. as shown in Fig. 8 (on the next page), for any $\pi _1\xrightarrow {0}_{\varepsilon }\pi _2,\ldots ,\pi _1\xrightarrow {0}_{\varepsilon }\pi _n$

  let $\pi '=\{\pi _1,\pi _2,\ldots ,\pi _n\}$ and

  • (1) $\pi _0\xrightarrow {}_{a}\pi _1$ implies $\pi _0\xrightarrow {}_{a}\pi ', a\in \Sigma ^s_t$,

  • (2) for any $\pi _j$ with $j=\{2,\ldots ,n\}, \pi _j\xrightarrow {}_{a}\pi '_j$ implies $\pi '\xrightarrow {}_{a}\pi '_j, a\in \Sigma ^s_t$.

Fig. 6

Step 1

Fig. 7

Step 2

Fig. 8

Step 3

Notice that: for any $\pi '=\{\pi _1,\ldots ,\pi _n\}\in \varPi ^s_t/\varPi$ and for any $x_a^i\in {\mathcal {V}}={\mathcal {V}}'-\{x_\varepsilon ^i\mid i=1,\ldots ,k\}$,

$$\begin{aligned} \overline{\delta _1}(x_a^i)=\cdots =\overline{\delta _n}(x_a^i). \end{aligned}$$

Hence, we denote the region related to $\pi '$ as $\overline{\delta '}$ which associates the same region to each resource-variable in ${\mathcal {V}}$.

Lemma 5

Given any $\mathcal {L}^t$ formula $\phi ^t$ closed w.r.t $B^t$. If $F(\phi ^t)$ is satisfiable in symbolic LWS $\mathcal {W}^s=(\varPi ^s,\Sigma ^s,\theta ^s)$, i.e. there exists $\pi =(\varGamma ,\overline{\delta })\in \varPi ^s$ s.t. $\mathcal {W}^s,\pi \models _{F(B^t)}F(\phi ^t)$. Then, there exists symbolic LWS $\mathcal {W}^s_t=(\varPi _t^s,\Sigma _t^s,\theta ^s_t)$ constructed as above, with $\pi '\in \varPi ^s_t$ s.t. either $\pi '=\pi$ or $\pi \in \pi '$ and $\mathcal {W}^s_t,\pi '\models _{B^t}\phi ^t$.

Proof

Induction on the structure of $\phi ^t$.

The cases $\bot ,\top ,\phi ^t\wedge \psi ^t,\phi ^t\vee \psi ^t$ and X are trivial.

• Case $x_a^i\bowtie r$:

  $\mathcal {W}^s,\pi \models _{F(B^t)}F(x_a^i\bowtie r)$ implies that for any $w\in \overline{\delta }(x_a^i), w\bowtie r$.

  If $\pi \in \varPi ^s_t$, then it is obvious that $\mathcal {W}^s_t,\pi \models _{B^t}x_a^i\bowtie r$.

  Otherwise, there exists $\pi '\in \varPi ^s_t$ s.t. $\pi \in \pi '$.

  As you mentioned above, $\overline{\delta '}(x^i_a)=\overline{\delta }(x)$ for any $x_a^i\in {\mathcal {V}}$.

  Hence, $\mathcal {W}^s_t,\pi '\models _{B^t}x_a^i\bowtie r$ also holds for this case.

• Case $[\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t$:

  $F([\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t)=[\varepsilon ][a](\bigwedge _{i\in I}(x_\varepsilon ^i\bowtie r_i)\rightarrow F(\phi ^t))$.

  Suppose there exist $\pi ',\pi '_1\in \varPi ^s_t$ s.t.

  • (1) $\pi '\xrightarrow {}_{a}\pi '_1$, and

  • (2) $w'_1-w'\bowtie r_i$ for any $i\in I$, $w'_1\in \overline{\delta '_1}(e^i)$ and $w'\in \overline{\delta '}(e^i)$.

  Then, there exists

  $\pi =(\varGamma ,\overline{\delta }),\pi _1=(\varGamma _1,\overline{\delta _1}), \pi _2=(\varGamma _2,\overline{\delta _2})\in \varPi ^s$ s.t.

  • 1. $\pi \xrightarrow {0}_{\varepsilon }\pi _1\xrightarrow {}_{a}\pi _2$ and

  • 2. $w_2-w_1\bowtie r_i$ for any $i\in I, w_2\in \overline{\delta _2}(e_i)$ and $w_1\in \overline{\delta _1}(e_i)$.

  $\pi \xrightarrow {0}_{\varepsilon }\pi _1$ implies that $\overline{\delta _1}(x_\varepsilon ^i)=0$ for any $x_\varepsilon ^i\in {\mathcal {V}}_\varepsilon$.

  Hence, for any $x_\varepsilon ^i\in {\mathcal {V}}_\varepsilon$ and any $w_2\in \overline{\delta _2}(x_\varepsilon ^i)$, we have $w_2\bowtie r_i$.

  That is equivalent to that for any $w_2\in \overline{\delta _2}(e_i)$ and $w_1\in \overline{\delta _1}(e_i)$, we have $w_2-w_1\bowtie r$.

  Since $\mathcal {W}^s,\pi \models _{F(B^t)}F([\bigwedge _{i\in I}(e_i\bowtie r_i)]_a\phi ^t)$, we have that $\mathcal {W}^s,\pi _2\models _{F(B^t)}F(\phi ^t)$.

  By inductive hypothesis, there exists $\pi '_2\in \varPi _t^s$ s.t.

  • 1. either $\pi '_2=\pi _2$ or $\pi _2\in \pi '_2$ and

  • 2. $\mathcal {W}^s_t,\pi '_2\models _{B^t}\phi ^t$.

  Hence, $\mathcal {W}^s_t,\pi '\models _{B^t}[{\bigwedge _{i\in I}(e_i\bowtie r_i)}]_a\phi ^t$.

• Case $\langle {\bigwedge _{i\in I}(e_i\bowtie r_i)}\rangle _a\phi ^t$:

  $F(\langle {\bigwedge _{i\in I}(e_i\bowtie r_i)}\rangle _a\phi ^t)=\langle {\varepsilon }\rangle \langle {a}\rangle (\bigwedge _{i\in I}(x_\varepsilon ^i\bowtie r_i)\wedge F(\phi ^t))$.

  $\mathcal {W}^s,\pi \models _{F(B^t)}F(\langle {\bigwedge _{i\in I}(e_i\bowtie r_i)}\rangle _a\phi ^t)$ implies that there exist $\pi _1=(\varGamma _1,\overline{\delta _1}),\pi _2=(\varGamma _2,\overline{\delta _2})\in \varPi ^s$ s.t.

  • 1. $\pi \xrightarrow {0}_{\varepsilon }\pi _1\xrightarrow {}_{a}\pi _2$,

  • 2. for any $i\in I, \overline{\delta _2}(x_\varepsilon ^i) \bowtie r_i$ and

  • 3. $\mathcal {W}^s,\pi _2\models _{F(B^t)}F(\phi ^t)$.

  $\pi \xrightarrow {0}_{\varepsilon }\pi _1$ implies that $\overline{\delta _1}(x_\varepsilon ^i)=0$ for any $x_\varepsilon ^i\in {\mathcal {V}}_\varepsilon$.

  Hence, $w_2-w_1\bowtie r_i$ for any $x_\varepsilon ^i\in {\mathcal {V}}_\varepsilon , w_2\in \overline{\delta _2}(x_\varepsilon ^i)$ and $w_1\in \overline{\delta _1}(x_\varepsilon ^i)$.

  That is equivalent to that $w_2-w_1\bowtie r_i$ for any $w_2\in \overline{\delta _2}(e_i)$ and $w_1\in \overline{\delta _1}(e_i)$.

  There exists $\pi '\in \varPi ^s_t$ s.t. $\pi ,\pi _1\in \pi '$, according to the construction of $\mathcal {W}^s_t$.

  By inductive hypothesis, $\mathcal {W}^s,\pi _2\models _{F(B^t)}F(\phi ^t)$ implies there exists $\pi '_2\in \varPi _t^s$ s.t.

  • 1. either $\pi '_2=\pi _2$ or $\pi _2\in \pi '_2$ and

  • 2. $\mathcal {W}^s_t,\pi '_2\models _{B^t}\phi ^t$.

    Hence, $\mathcal {W}^s_t,\pi '\models _{B^t}\langle {\bigwedge _{i\in I}(e_i\bowtie r_i)}\rangle _a\phi ^t$.$\square$

By the above-introduced method, one can construct the symbolic model for a given $\mathcal {L}^t$ formula—if satisfiable. Then, we can use the technique in Lemma 1 to generalize an LWS $\mathcal {W}=({M},{\mathcal {K}},\Sigma ,\theta ),$ which is a model for the given $\mathcal {L}^t$ formula.

Theorem 4

(Decidability of $B^t$-satisfiability for $\mathcal {L}^t$) For an arbitrary maximal equation block $B^t$, the $B^t$-satisfiability problem for $\mathcal {L}^t$ is decidable.

7 Conclusion

In this paper, we developed two recursive versions of the weighted modal logic (Larsen and Mardare 2014) $\mathcal {L}^w$ and $\mathcal {L}^t$. They use a semantics based on labelled weighted transition systems (LWSs). This type of transition systems is used to describe systems involving various types of quantitative information. These models involve a number of resources that label both transitions and states. In particular, the transitions are labelled simultaneously with both actions and real values representing the costs of the corresponding transitions in term of resources.

The two RWLs, $\mathcal {L}^w$ and $\mathcal {L}^t$, encode qualitative and quantitative properties of LWSs. With respect to the weighted logics studied before, $\mathcal {L}^w$ and $\mathcal {L}^t$ make use of recursive variables that allow us to encode circular properties and infinite behaviours, including safety and cost-bounded liveness properties. The RWLs use first-order resource-variables to measure local costs. The main syntactic operators are similar to the ones of timed logics for real-time systems. $\mathcal {L}^w$ has operators that constrain the value of resource-variables at the current state. $\mathcal {L}^t$ extends $\mathcal {L}^w$ by having quantitative constraints on the transition modalities as well. This extension makes sure that $\mathcal {L}^t$ is adequate (while $\mathcal {L}^w$ is not), i.e. the semantic equivalence induced by $\mathcal {L}^t$ coincides with the weighted bisimilarity of LWSs.

Even though $\mathcal {L}^w$ is the least expressive of the two logics discussed in this paper, it fails to enjoy the finite model property. However, we proved that the satisfiability problem for $\mathcal {L}^w$ is still decidable. By applying a variant of the region construction technique developed for timed automata, we obtained symbolic LWSs of the satisfiable $\mathcal {L}^w$ formulas. These symbolic LWSs provide an abstract semantics for LWSs, allowing us to reason about satisfiability by investigating the symbolic models that are finite. We have proposed a model construction algorithm, which constructs a symbolic LWS for a given satisfiable (consistent) $\mathcal {L}^w$ formula. The symbolic model can be eventually used to determine the existence of the concrete LWSs and generate them. The systems are possibly infinitely.

The satisfiability problem of $\mathcal {L}^t$ can be solved in a similar way with $\mathcal {L}^w$. However, we provided an attractive alternative: firstly, encode the problem for $\mathcal {L}^t$ into one similar to that of $\mathcal {L}^w$ by translating the given $\mathcal {L}^t$ formula into $\mathcal {L}^w$ with a special 0-cost action; secondly, use the model construction algorithm with a minor modification to check the satisfiability of this $\mathcal {L}^w$ formula; and finally, if the $\mathcal {L}^w$ formula is not satisfiable, then the given $\mathcal {L}^t$ formula is not satisfiable either; otherwise, the given $\mathcal {L}^t$ formula is satisfiable and the model for it can be eventually generated according to the model for the corresponding $\mathcal {L}^w$ formula.