[a,b] [a]

# Asynchronous Composition of LTL Properties over Infinite and Finite Traces

Alberto Bombardelli 0000-0003-3385-3205  and  Stefano Tonetta
0000-0001-9091-7899  Fondazione Bruno Kessler, via Sommarive 18, Trento Italy
380123<EMAIL_ADDRESS><EMAIL_ADDRESS>University of Trento, via
Sommarive 16, Trento Italy 380123<EMAIL_ADDRESS>
###### Abstract.

The verification of asynchronous software components poses significant
challenges due to the way components interleave and exchange input/output data
concurrently. Compositional strategies aim to address this by separating the
task of verifying individual components on local properties from the task of
combining them to achieve global properties. This paper concentrates on
employing symbolic model checking techniques to verify properties specified in
Linear-time Temporal Logic (LTL) on asynchronous software components that
interact through data ports. Unlike event-based composition, local properties
can now impose constraints on input from other components, increasing the
complexity of their composition. We consider both the standard semantics over
infinite traces as well as the truncated semantics over finite traces to allow
scheduling components only finitely many times.

We propose a novel LTL rewriting approach, which converts a local property
into a global one while considering the interleaving of infinite or finite
execution traces of components. We prove the semantic equivalence of local
properties and their rewritten version projected on the local symbols. The
rewriting is also optimized to reduce formula size and to leave it unchanged
when the temporal property is stutter invariant. These methods have been
integrated into the OCRA tool, as part of the contract refinement verification
suite. Finally, the different composition approaches were compared through an
experimental evaluation that covers various types of specifications.

##  1\. Introduction

Software model checking [Roz11, BK08] is a technique employed. It combines a
variety of methods based on deductive reasoning, abstraction, and state space
exploration. Model checking typically specifies the property to be verified in
a temporal logic. One of the most common logic used to express properties of
programs is Linear-time Temporal Logic (LTL) [Pnu77].

Software model checking [Roz11, BK08] is a technique employed for the
verification of complex programs. This approach combines different methods
based on deductive reasoning, state space exploration and abstract to prove
whether or not a given property is satisfied. In most cases, properties are
expressed either as invariants or as temporal properties; in particular, one
of the most common logic used for programs is Linear-time Temporal Logic (LTL)
[Pnu77].

State space explosion is one of the main problems for the scalability of model
checking. The problem worsens when considering the asynchronous composition of
programs, due to the non-deterministic interleaving of components and
concurrent access to shared variables. Compositional techniques are often used
to tackle scalability issues. The idea of this approach is to decouple the
problem of verifying local properties specified over the component interfaces
from the problem of composing them to ensure some global property.

For example, in [RBH+01] is described the following compositional reasoning.
Given some local component ($\mathcal{M}_{1},\dots,\mathcal{M}_{n}$), some
local properties of these components ($\varphi_{1},\dots,\varphi_{n}$), a
global property ($\varphi$), a notion of composition for the components
($\gamma_{S}$) and a notion of composition for the properties ($\gamma_{P}$);
if the local components satisfy the local properties and the composition of
local properties entails the global properties, the local component
composition satisfies the global property. Although this reasoning is general,
the asynchronous composition of local temporal properties may be tricky when
considering software components communicating through data ports.

In this paper, we define the asynchronous composition of LTL properties local
to components; which means that the local properties reason only over the part
of the execution of the local component, e.g., when a local property refers to
the next state, the composition will consider the next state such that the
local component is running. The communication between local components is
achieved with I/O data ports while their execution is controlled by scheduling
constraints. Due to uncontrollable input changes, the composition must take
into account whether or not the local component is running even if the formula
does not contain ”next”111Usually when an LTL formula does not contain next is
stutter invariant. In such cases, the asynchrony would not interfere with the
formula.. Another important factor to consider is the possibly finite
execution of local components. If for instance, the scheduler is not fair, the
unlucky local component might be scheduled only for a finite amount of time.
This ”possibly finite” local semantics also allow for a natural way to
represent permanent faults in asynchronous systems (e.g. a local component is
not scheduled anymore means that it crashed).

Our approach is based on a syntactical rewriting $\mathcal{R}^{*}_{c}$ of the
local temporal property to a property of the composite model. The rewriting is
then conjoined with a constraint ensuring that output variables do not change
when the component is not running ($\psi_{cond}$). The property composition
$\gamma_{P}$ is in the following form: $\psi_{cond}\wedge\bigwedge_{1\leq
i\leq n}\mathcal{R}^{*}_{i}(\varphi_{i})$.

To represent the ”possibly finite” local semantics, we use the truncated weak
semantics defined in [EFH+03a] to represent local properties. The idea is that
the local formula can be interpreted to both finite and infinite trace, and
the formula semantics does not force the system to execute the local
component. For completeness, we define the composition in a way that soundly
supports the finite execution of the composed system as well; therefore, the
compositional reasoning applies to hierarchical systems too.

The proposed approach has been implemented inside OCRA[CDT13], which allows a
rich extension of LTL and uses a state-of-the-art model checking algorithm
implemented in nuXmv [CCD+14] as back-ends to check satisfiability.

In this paper, we present the rewriting in two distinct forms: (i) a form
which supports the local ”possibly-finite” semantics, (ii) a form optimized
for infinite local executions.

We evaluated our approach on models representing compositions of pattern
formulas and real models from the automotive domains [CCG+23]. We show both
the qualitative differences in results between the two semantics and the
impact of the optimization when dealing with local infinite executions.

###  1.1. Motivating examples

We propose two examples to motivate our work. The first model is a toy example
representing a system that tries to send a value to a network while the second
is a real model coming from the automotive domain. Both models can be
naturally represented through possibly finite scheduling of local components.

####  1.1.1. Sender

We now model a three-component system that represents a system that receives a
message and tries to send it through a network. The component either
successfully delivers the message or fails to send it and logs the message.
The example is represented in Figure 1. This example is composed of three
components: Component $c1$ receives a message $rec_{1}$ and an input $in_{1}$
and tries to send the value to component $c2$. If $c1$ is eventually able to
send $send_{2}$ message through the network, then $c2$ will run and will
output the original input. The network guarantees that eventually, $c1$ will
be able to send the message to $c2$; however, if $c1$ runs only finitely many
times, $c3$ at some point will report a failure. The global property states
that if an input message is received, it is either eventually delivered as
output or an error occurs. If $c1$ runs infinitely often, the global property
is satisfied without the need for $c3$.

$c1$$c2$$c3$$rec$$in$$o_{1}$$i_{2}$$o_{f}$$fail$$send$$try_{1}$$try$$send_{1}$$rec_{2}$$o$$i_{3}$

$\displaystyle\varphi_{c1}:=$ $\displaystyle G(rec_{1}\rightarrow
out_{1}^{\prime}=in_{1}\wedge X((try_{1}\wedge
out_{1}^{\prime}=out_{1})Usend_{1}))$ $\displaystyle\varphi_{c2}:=$
$\displaystyle G(rec_{2}\rightarrow out2^{\prime}=in2\wedge Xsend_{2})$
$\displaystyle\varphi_{c3}:=$ $\displaystyle G(try_{3}\rightarrow
out_{f}^{\prime}=in_{3}\wedge Xfail)$ $\displaystyle\varphi:=$ $\displaystyle
G(rec\wedge in=v\rightarrow F(send\wedge out=v\vee fail\wedge out_{f}=v)$
$\displaystyle\alpha:=$ $\displaystyle G(in_{1}\rightarrow run_{1})\wedge$
$\displaystyle G(send_{1}\rightarrow run_{2})\wedge$ $\displaystyle G(H_{\leq
p}try_{1}\rightarrow run_{3})$

Figure 1. Figure representing the sender model. The colour red represents
input variables while the colour blue represents the output variables.

####  1.1.2. Automotive compositional contract

Another interesting example comes from the automotive domain. In [CCG+23], the
EVA framework was proposed for the compositional verification of AUTOSAR
components. That work used the rewriting technique we proposed in [BT22] to
verify the correct refinement of contracts defined as a pair of LTL
properties.

Due to the complexity of the model, we omit a full description of the system,
the specifications and the properties. We focus on a specific requirement of
the system that states that the system shall brake when the Autonomous
Emergency Braking module gets activated. A simplified version of the
specification is defined by the following LTL formula:

$G(X(aeb\\_breaking.status\neq 0)\rightarrow
F_{[0,2]}Brake\\_\\_In\\_\\_BrakeActuator\neq 0)$

The specification is entailed by a brake actuator component that is composed
of the actual actuator (BrakeActuator#BA_Actuator) and a watchdog
(BrakeActuator#BA_Watchdog). The actuator is scheduled every time a signal is
received in input while the watchdog is scheduled periodically. By reasoning
over finite executions of components, it is possible to verify whether or not
the global specification is valid even if at some point the Actuator stop
working.

###  1.2. Overall contribution

The main contribution of this paper is the definition of a rewriting-based
technique to verify compositional asynchronous systems in a general way.
Furthermore, we provide an additional optimized rewriting technique to cover
the case in which local components are assumed to run infinitely often. The
main advantages of our compositional approach are the following:

  * •

It supports asynchronous communication between data ports.

  * •

It supports generic scheduling constraints expressible through LTL formulas.

  * •

It supports both finite and infinite executions of local components making it
a suitable approach for safety assessment as well.

This work is an extension of the conference paper [BT22]. The work has been
extended with the following contributions:

  * •

A weak semantics for the logic with two decision procedures for its
verification.

  * •

A new definition of asynchronous composition of Interface Symbolic Transition
Systems that deals with possibly finite execution of components.

  * •

A new rewriting that generalizes the previous one for possibly finite systems

  * •

A new experimental evaluation with new models and a set of benchmarks from the
automotive domain.

###  1.3. Outline

The rest of the paper is organized as follows: in Sec. 2, we compare the
proposed solution with related works; in Sec. 3, we define our logic syntax,
semantics and verification; in Sec. 4, we formalize the problem; in Sec. 5, we
define the rewriting approach, its basic version, its complete version and an
optimized variation that is suited for infinite executions only; in Sec. 6, we
report on the experimental evaluation; finally, in Sec. 7, we draw the
conclusions and some directions for future works.

##  2\. Related works

One of the most important works on temporal logic for asynchronous systems is
Temporal Logic of Action (TLA) [Lam94] by Leslie Lamport, later extended with
additional operators[Lam97]. TLA has been also used in a component-based
manner in [RR09]. Our formalism has similarities with TLA. We use a
(quantifier-free) first-order version of LTL [MP92b] with “next” function to
specify the succession of actions of a program. TLA natively supports the
notion of stuttering for composing asynchronous programs so that the
composition is simply obtained by conjoining the specifications. We focus
instead on local properties that are specified independently of how the
program is composed so that “next” and input/output data refer only to the
local execution. Another substantial difference with TLA is that our formalism
also supports a finite semantics of LTL, permitting reason over finite traces.

As for propositional LTL, the composition of specifications is studied in
various papers on assume-guarantee reasoning (see, e.g., [McM99, PDH99, JT96,
CT15a]) for both synchronous and asynchronous composition. In the case of
asynchronous systems, most works focus on fragments of LTL without the next
operator, where formulas are always stutter invariant. Other studies
investigated how to tackle down state-space explosion for that scenario
usually employing techniques such as partial order reduction [BBC+09].
However, our work covers a more general setting, where the presence of input
variables makes formulas non-stutter-invariant.

Similar to our work, [BBC+09] considers a rewriting for LTL with events to map
local properties into global ones with stuttering. However, contrary to this
paper, it does not consider input variables (nor first-order extension) and
assume that every variable does not change during stuttering, resulting in a
simpler rewriting. In [EFH+03b], a temporal clock operator is introduced to
express properties related to multiple clocks and, in principle, can be used
to interpret formulas over the time points in which a component is not
stuttering. Its rewriting is indeed similar to the basic version defined in
this paper, but is limited to propositional LTL and has not been conceived for
asynchronous composition. The optimization that we introduce to exploit the
stutter invariance of subformulas results in simpler formulas easy to be
analyzed as shown in our experimental evaluation.

The rewriting of asynchronous LTL is similar to the transformation of
asynchronous symbolic transition systems into synchronous ones described in
[CMT11]. The work considers connections based on events where data are
exchanged only upon synchronization (allowing optimizations as in shallow
synchronization [BCL+10]). Thus, it does not consider components that read
from input variables that may be changed by other components. Moreover,
[CMT11] is not able to transform temporal logic local properties in global
ones as in this paper. In [LBA+22], the authors defined a technique to verify
asynchronous assume/guarantee systems in which assumptions and guarantees are
defined on a safety fragment of LTL with predicates and functions. The main
differences between that work and this one are the following. The logic
considered by [LBA+22] is limited to a safety fragment of LTL with “globally”
and past operators; on the other hand, our work covers full LTL with past
operators with event freezing functions and finite semantics. Another key
difference is that they consider scheduling in which a component is first
dispatched and then, after some steps it completes its action; instead, our
framework defines scheduling constraints with LTL formulas and actions are
instantaneous.

Finally, our logic semantics is based on the works of Eisner, Fisman et al on
truncated LTL of [EFH+03a]. The main differences are the following. Our logic
includes past operators, first-order predicates and functions; we consider
only weak/strong semantics for our logic while their work instead also deals
with neutral semantics.

##  3\. First Order Past LTL with weak truncated semantics

This section presents the syntax and the semantics of the logic used in this
paper and its verification.

The logic is an extension of LTL with event-freezing functions of [Ton17] that
is interpreted over both finite and infinite traces. As we mentioned in the
introduction, we are considering weak semantics for our logic that is based on
the works of Eisner and Fisman[EFH+03a, FK18]. The overall idea behind this
logic is to have an expressive language that can reason on both infinite and
truncated executions of programs. Finally, we can observe that for each
infinite trace, if the trace satisfies a property, then all its finite prefix
satisfies it as well under the weak semantics.

Prior to the logic, we denote the notion of trace. In this paper, traces can
be both finite and infinite. Moreover, in this paper, traces distinguish
between input and output symbols.

We define a trace $\pi$ as a sequence $s_{0},s_{1},\dots$ of assignments over
a set of input variables $V^{I}$ and output variables $V^{O}$. A trace $\pi$
is denoted as finite if the sequence of assignments $s_{0},s_{1},\dots$ is
finite. Moreover, if a trace is finite, its last assignment is defined over
the symbols of $V^{O}$. We denote the set of traces finite and infinite over
$V^{I},V^{O}$ as $\Pi(V^{I},V^{O})$.

###  3.1. Syntax

In this paper, we consider LTL [MP92a] extended with past operators [LPZ85] as
well as “if-then-else” ($ite$) and “at next” ($@\tilde{F}$), and “at last”
($@\tilde{P}$) operators from [Ton17]. For simplicity, we refer to it simply
as LTL.

We work in the setting of Satisfiability Modulo Theory (SMT) [BSST09] and LTL
Modulo Theory (see, e.g., [CGM+19]). First-order formulas are built as usual
by proposition logic connectives, a given set of variables $V$ and a first-
order signature $\Sigma$, and are interpreted according to a given
$\Sigma$-theory $\mathcal{T}$. We assume to be given the definition of
$M,\mu\models\mathcal{T}\varphi$ where $M$ is a $\Sigma$-structure, $\mu$ is a
value assignment to the variables in $V$, and $\varphi$ is a formula. Whenever
$\mathcal{T}$ and $M$ are clear from contexts we omit them and simply write
$\mu\models\varphi$. Given a signature $\Sigma$ and a set of variables $V$,
LTL formulas $\varphi$ are defined by the following syntax:

$\varphi:=\top|\bot|pred(u_{1},\dots,u_{n})|\neg\varphi_{1}|\varphi_{1}\vee\varphi_{2}|X\varphi_{1}|\varphi_{1}U\varphi_{2}|Y\varphi_{1}|\varphi_{1}S\varphi_{2}$
$u:=c|x|func(u_{1},\dots,u_{n})|next(u_{1})|ite(\varphi,u_{1},u_{2})|u_{1}@\tilde{F}\varphi|u_{1}@\tilde{P}\varphi$

where $c$, $func$, and $pred$ are respectively a constant, a function, and a
predicate of the signature $\Sigma$ and $x$ is a variable in $V$.

Apart from $@\tilde{F}$ and $@\tilde{P}$, the operators are standard.
$u@\tilde{F}\varphi$ represents the value of $u$ at the next point in time in
which $\varphi$ holds. Similarly, $u@\tilde{P}\varphi$ represents the value of
$u$ at the last point in time in which $\varphi$ holds.

######  Example .

We provide an example of our logic from [Ton17] representing a sensor. In this
example, the sensor has an input real variable $y$, an output real variable
$x$ and a Boolean flag $correct$ that represents whether or not the value
reported by the sensor is correct. We specify that $x$ is always equal to the
last correct input value with $G(x=y@\tilde{P}(correct))$. We assume that a
failure is permanent with $G(\neg correct\rightarrow G\neg correct)$.
Additionally, we consider also a Boolean variable $read$ representing the
event of reading $x$. In our example, $reading$ occurs periodically with
period $5$: $read\wedge G(read\rightarrow X(G^{\leq 3}\neg read)\wedge
X^{5}read)$. Finally, let us say that an alarm $a$ is true if and only if the
last two read values are the same: $G(a\leftrightarrow
x@\tilde{P}(read)=(x@\tilde{P}(read))@\tilde{P}(read))$.

We can prove that, given the behaviour defined above, every point at which the
sensor is not correct, is followed by an alarm in at most $10$ steps.

$\displaystyle(G(x=y@\tilde{P}(correct))\wedge G(\neg correct\rightarrow G\neg
correct)\wedge$ $\displaystyle read\wedge G(read\rightarrow X(G^{\leq 3}\neg
read)\wedge X^{5}read)\wedge$ $\displaystyle G(a\leftrightarrow
x@\tilde{P}(read)=(x@\tilde{P}(read))@\tilde{P}(read)))$
$\displaystyle\rightarrow G(\neg correct\rightarrow F^{\leq 10}a)$

###  3.2. Semantics

We propose an alternative semantics for LTL with past operators and event
freezing function based on the truncated semantics of LTL defined in
[EFH+03a]. This semantics is tailored for both finite and infinite traces. For
what regards infinite traces, the semantics is identical to the standard one.
When we reason over finite traces, the predicates are interpreted “weakly”
i.e. all the predicates are evaluated as true at the end of the trace.
Moreover, the semantics differentiate between output and input predicates by
treating the latter as next operators i.e. they are evaluated as true in the
last state.

Another important difference between standard LTL and other finite semantics
(e.g. $LTL_{f}$[DGV13]) lies in the negation. When a formula is negated the
interpretation passes from weak to strong and vice versa. Therefore, a negated
formula $\neg\phi$ is satisfied with weak (strong) semantics if and only if
$\phi$ is not satisfied with strong (weak) semantics. This means for instance
that a proposition $P$ is evaluated as true at the end of a trace independent
of the polarity of its variables.

Contrary to the original truncated semantics of [EFH+03a], we consider also
past operators, if-then-else, event freezing operators
($@\tilde{F},@\tilde{P}$), functions and terms.

For what regards past operators, the semantics is similar to standard LTL. The
only alteration of the past semantics is that $Y$ is evaluated as true at the
end of the trace. This is done to keep the value of each formula trivially
true when evaluated outside of the trace bounds.

In this paper, terms are not evaluated with a polarity because they are
interpreted inside predicates. Besides $ite,@\tilde{F},@\tilde{P}$, these
operators are interpreted identically to standard LTL.

For if-then-else, instead of considering 2 possible term interpretations
($u_{1},u_{2}$), the new semantics consider a third default value. The third
value is chosen when both the if condition and its negation are satisfied
weakly. This choice of semantics guarantees that
$v=ite(\varphi,u_{1},u_{2})\equiv(\varphi\rightarrow
v=u_{1})\wedge(\neg\varphi\rightarrow v=u_{2})$.

Regarding $\varphi@\tilde{F}u$ and $\varphi@\tilde{P}u$, the new semantics
considers strong satisfaction of the formula to get the value of the term.
This occurs because strong semantics ensures that variables are well-defined
in the trace.

The semantics is defined as follows:

  * •

$\pi,M,i\models_{t^{-}}pred^{O}(u_{1},\dots,u_{n})\text{ iff }|\pi|\leq
i\text{ or }pred^{M}(\pi^{M}(i)(u_{1}),\dots,\pi^{M}(i)(u_{n}))$

  * •

$\pi,M,i\models_{t^{+}}pred^{O}(u_{1},\dots,u_{n})\text{ iff }|\pi|>i\text{
and }pred^{M}(\pi^{M}(i)(u_{1}),\dots,\pi^{M}(i)(u_{n}))$

  * •

$\pi,M,i\models_{t^{-}}pred^{I}(u_{1},\dots,u_{n})\text{ iff }|\pi|\leq
i-1\text{ or }pred^{M}(\pi^{M}(i)(u_{1}),\dots,\pi^{M}(i)(u_{n}))$

  * •

$\pi,M,i\models_{t^{+}}pred^{I}(u_{1},\dots,u_{n})\text{ iff }|\pi|>i+1\text{
and }pred^{M}(\pi^{M}(i)(u_{1}),\dots,\pi^{M}(i)(u_{n}))$

  * •

$\pi,M,i\models_{t^{sgn}}\varphi_{1}\wedge\varphi_{2}\text{ iff
}\pi,M,i\models_{t^{sgn}}\varphi_{1}\text{ and
}\pi,M,i\models_{t^{sgn}}\varphi_{2}$

  * •

$\pi,M,i\models_{t^{-}}\neg\varphi\text{ iff
}\pi,M,i\not\models_{t^{+}}\varphi$

  * •

$\pi,M,i\models_{t^{+}}\neg\varphi\text{ iff
}\pi,M,i\not\models_{t^{-}}\varphi$

  * •

$\pi,M,i\models_{t^{sgn}}\varphi_{1}{U}\varphi_{2}\text{ iff there exists
}k\geq i,\pi,M,k\models_{t^{sgn}}\varphi_{2}\text{ and for all }l,i\leq
l<k,\pi,M,l\models_{t^{sgn}}\varphi_{1}$

  * •

$\pi,M,i\models_{t^{-}}\varphi_{1}{S}\varphi_{2}\text{ iff }i\geq|\pi|\text{
or there exists }k\leq i,\pi,M,k\models_{t^{-}}\varphi_{2}\text{ and for all
}l,k<l\leq i,\pi,M,l\models_{t^{sgn}}\varphi_{1}$

  * •

$\pi,M,i\models_{t^{sgn}}X\varphi\text{ iff
}\pi,M,i+1\models_{t^{sgn}}\varphi$

  * •

$\pi,M,i\models_{t^{-}}Y\varphi\text{ iff }i\geq|\pi|\text{ or }i>0\text{ and
}\pi,M,i-1\models_{t^{-}}\varphi$

  * •

$\pi,M,i\models_{t^{+}}Y\varphi\text{ iff }0<i<|\pi|\text{ and
}\pi,M,i-1\models_{t^{+}}\varphi$

where $pred^{I}$ denotes a predicate containing input variables or
$@\tilde{F}$ terms, $pred^{O}$ denotes a predicate that contains only output
variables without at next and $pred^{M}$ is the interpretation $M$ of the
predicate in $\Sigma$.

The interpretation of terms $\pi^{M}(i)$ is defined as follows:

  * •

$\pi^{M}(i)(c)=c^{M}$

  * •

$\pi^{M}(i)(x)=s_{i}(x)$ if $x\in V$

  * •

$\pi^{M}(i)(func(u_{1},\dots,u_{n}))=func^{M}(\pi^{M}(i)(u_{1}),\ldots,\pi^{M}(i)(u_{n}))$

  * •

$\pi^{M}(i)(u@\tilde{F}(\varphi))=\pi^{M}(k)(u)\text{if there exists
}k>i\text{ such that, for all }l,i<l<k,\pi,M,l\models_{t^{+}}\neg\varphi\text{
and }\pi,M,k\models_{t^{+}}\varphi$;
$\pi^{M}(i)(u@\tilde{F}(\varphi))=def_{u@\tilde{F}\varphi}$ otherwise.

  * •

$\pi^{M}(i)(u@\tilde{P}(\varphi))=\pi^{M}(k)(u)\text{if}i<|pi|\text{ and there
exists }k<i\text{ such that, for all
}l,i>l>k,\pi,M,l\models_{t^{+}}\neg\varphi\text{ and
}\pi,M,k\models_{t^{+}}\varphi$;
$\pi^{M}(i)(u@\tilde{P}(\varphi))=def_{u@\tilde{P}\varphi}$ otherwise.

  * •

$\pi^{M}(i)(ite(\varphi,u_{1},u_{2}))=\begin{cases}\pi^{M}(i)(u_{1})&\text{ if
}\pi,M,i\models_{t^{+}}\varphi\\\
\pi^{M}(i)(u_{2})&\pi,M,i\models_{t^{+}}\neg\varphi\\\
def_{ite(\varphi,u_{1},u_{2})}&\text{ otherwise}\end{cases}$

where $func^{M},c^{M}$ are the interpretation $M$ of the symbols in $\Sigma$,
and $def_{u@\tilde{F}\varphi}$, $def_{u@\tilde{P}\varphi}$ and
$def_{ite(\varphi,u_{1},u_{2})}$ are some default values in the domain of $M$.

Finally, we have that $\pi,M\models_{t}\varphi\text{ iff
}\pi,M,0\models_{t^{-}}\varphi$.

######  Example .

Here we provide a short example to clarify the semantics. Suppose that a local
component is represented by a temporal property $\varphi_{i}:=G(i\rightarrow
Xo)$; the property expresses that, if the input $i$ is received, at the next
step in the local trace the output $o$ is provided. In our semantics, this
means that the execution $\pi_{f}=\\{i\\},\\{o\\},\\{o,i\\},\\{o\\}$ is
satisfied by the property, but since the semantics is weak also
$\pi_{f}^{\prime}=\\{o,i\\}\\{o\\},\\{i\\}$ satisfies the property according
to the semantics. It should be noted that when we reason over infinite
executions, the truncated weak semantics is identical to the standard
semantics; therefore, this semantics can be interpreted as a generalisation of
the standard one.

###  3.3. Notation simplification

In the following, we assume to have a background theory such that the symbols
in $\Sigma$ are interpreted by an implicit structure $M$ (e.g., theory of
reals, integers, etc.). We therefore omit $M$ to simplify the notation,
writing $\pi,i\models_{t^{sgn}}\varphi$ and $\pi(i)(u)$ instead of
respectively $\pi,M,i\models_{t^{sgn}}\varphi$ and $\pi^{M}(i)(u)$.

Finally, we use the following standard abbreviations:
$\varphi_{1}\wedge\varphi_{2}:=\neg(\neg\varphi_{1}\vee\neg\varphi_{2})$,
$\varphi_{1}R\varphi_{2}:=\neg(\neg\varphi_{1}U\neg\varphi_{2})$
($\varphi_{1}$ releases $\varphi_{2}$), $F\varphi:=\top U\phi$ (sometime in
the future $\varphi$), $G\varphi:=\neg F\neg\varphi$ (always in the future
$\varphi$), $O\varphi:=\top S\varphi$ (once in the past $\varphi$),
$H\varphi:=\neg O\neg\varphi$ (historically in the past $\varphi$),
$Z\varphi:=\neg Y\neg\varphi$ (yesterday $\varphi$ or at initial state),
$X^{n}\varphi:=XX^{n-1}\varphi$ with $X^{0}\varphi:=\varphi$,
$Y^{n}\varphi:=YY^{n-1}\varphi$ with $Y^{0}\varphi:=\varphi$,
$Z^{n}\varphi:=ZZ^{n-1}\varphi$ with $Z^{0}\varphi:=\varphi$, $F^{\leq
n}\varphi:=\varphi\vee X\varphi\vee\cdots\vee X^{n}\varphi$, $G^{\leq
n}\varphi:=\varphi\wedge X\varphi\wedge\cdots\wedge X^{n}\varphi$, $O^{\leq
n}\varphi:=\varphi\vee Y\varphi\vee\cdots\vee Y^{n}\phi$, $H^{\leq
n}\varphi:=\varphi\wedge Z\varphi\wedge\cdots\wedge Z^{n}\varphi$.

###  3.4. Verification

We present two techniques to verify LTL formulae with truncated semantics. The
first technique is a variation of the rewriting proposed in [DGV13]. It
reduces the verification of finite semantics to standard LTL semantics by
introducing a $Tail$ variable representing the end of the trace. We define
$Tr(\varphi)$ as follows:

$\displaystyle Tr^{-}(Pred^{I}):=Tail\vee Pred^{I}\quad Tr^{+}(Pred^{I}):=\neg
Tail\wedge Pred^{I}$ $\displaystyle Tr^{sgn}(Pred^{O}):=Pred^{O}\quad\quad
Tr^{sgn}(\varphi_{1}\vee\varphi_{2}):=Tr^{sgn}(\varphi_{1})\vee
Tr^{sgn}(\varphi_{2})$ $\displaystyle Tr^{-}(\neg\varphi)=\neg
Tr^{+}(\varphi)\quad Tr^{+}(\neg\varphi)=\neg Tr^{-}(\varphi)$ $\displaystyle
Tr^{-}(X\varphi):=X(Tail\vee Tr^{-}(\varphi))\quad Tr^{+}(X\varphi):=X(\neg
Tail\wedge Tr^{+}(\varphi))$ $\displaystyle
Tr^{-}(\varphi_{1}U\varphi_{2}):=Tr^{-}(\varphi_{1})U(Tail\vee
Tr^{-}(\varphi_{2}))$ $\displaystyle
Tr^{+}(\varphi_{1}U\varphi_{2}):=Tr^{+}(\varphi_{1})U(\neg Tail\wedge
Tr^{+}(\varphi_{2}))$

where $Tr(\varphi):=\neg Tail\wedge G(Tail\rightarrow XTail)\rightarrow
Tr^{-}(\varphi)$

The second technique reduces the problem to the verification of safetyLTL
fragment. The idea is that the property is valid on the truncated semantics
iff the property is valid with standard semantics and its ”safety part” is
valid with truncated semantics. The verification of the safety fragment is
carried out reducing the problem to invariant checking. Contrary to the
standard semantics, in our setting it is not necessary to check that the
finite trace is extendible as done instead in [BCTZ23]. The reduction from
safetyLTL to invariant is based on [CGH94, Lat03, KV01] and have been detailed
practically in [BCTZ23]. In the following, we propose the rewriting to
transform a formula from LTL to safetyLTL. The transformation is performed by
replacing until with release on the formula in negative normal form (see
Definition 3.4 below).

Given a formula $\varphi$ in negative normal form, we define
$\mathcal{W}2\mathcal{S}(\varphi)$ as:

$\displaystyle\mathcal{W}2\mathcal{S}(Pred):=Pred\quad\mathcal{W}2\mathcal{S}(\neg
Pred):=\neg Pred$
$\displaystyle\mathcal{W}2\mathcal{S}(\varphi_{1}\vee\varphi_{2}):=\mathcal{W}2\mathcal{S}(\varphi_{1})\vee\mathcal{W}2\mathcal{S}(\varphi_{2})\quad\mathcal{W}2\mathcal{S}(\varphi_{1}\wedge\varphi_{2}):=\mathcal{W}2\mathcal{S}(\varphi_{1})\wedge\mathcal{W}2\mathcal{S}(\varphi_{2})$
$\displaystyle\mathcal{W}2\mathcal{S}(X\varphi):=X\mathcal{W}2\mathcal{S}(\varphi)\quad\mathcal{W}2\mathcal{S}(Y\varphi):=Y\mathcal{W}2\mathcal{S}(\varphi)$
$\displaystyle\mathcal{W}2\mathcal{S}(\varphi_{1}U\varphi_{2}):=\mathcal{W}2\mathcal{S}(\varphi_{2})R(\mathcal{W}2\mathcal{S}(\varphi_{1})\vee\mathcal{W}2\mathcal{S}(\varphi_{2}))$
$\displaystyle\mathcal{W}2\mathcal{S}(\varphi_{1}R\varphi_{2}):=\mathcal{W}2\mathcal{S}(\varphi_{1})R(\mathcal{W}2\mathcal{S}(\varphi_{2}))$

######  Theorem 1.

$\mathcal{M}\models_{t^{-}}\varphi\Leftrightarrow\mathcal{M}\models_{LTL}\varphi\text{
and }\mathcal{M}\models_{t}\mathcal{W}2\mathcal{S}(\varphi)$

######  Proof 3.1.

We can prove the theorem by induction on the structure of the formula. We
prove the theorem considering each trace $\pi$ and index $i$ i.e. we prove
$\pi,i\models_{t^{-}}\varphi$. We need to prove only the case of the operator
$U$ since $\mathcal{W}2\mathcal{S}$ is transparent for the other operators.
Moreover, we need to prove only weak semantics because the top level formula
is in negative normal form.

  * •

If $\pi$ is an infinite trace,
$\pi,i\models_{t^{-}}\varphi_{1}U\varphi_{2}\Leftrightarrow\pi,i\models\varphi_{1}U\varphi_{2}$.

  * •

If $|\pi|=n$:
$\pi,i\models_{t^{-}}\varphi_{1}U\varphi_{2}\Leftrightarrow\exists k\geq
i\text{ s.t. }\pi,k\models_{t^{-}}\varphi_{2}\text{ and }\forall i\leq
j<k:\pi,j\models_{t^{-}}\varphi_{1}\Leftrightarrow\pi,i\models_{t^{-}}\mathcal{W}2\mathcal{S}(\varphi_{1})U\mathcal{W}2\mathcal{S}(\varphi_{2})\Leftrightarrow\exists
k\geq i\text{ s.t. }(k<n\text{ and
}\pi,k\models_{t^{-}}\mathcal{W}2\mathcal{S}(\varphi_{1})\text{ or }k=n)\text{
for all }i\leq
j<k:\pi,j\models_{t^{-}}\mathcal{W}2\mathcal{S}(\varphi_{1})\Leftrightarrow\forall
i\leq j<n:\pi,j\models\varphi_{1}\text{ or }\exists i\leq
k<n:\pi,k\models_{t^{-}}\mathcal{W}2\mathcal{S}(\varphi_{2})\text{ and
}\forall i\leq
j<k:\pi,j\models_{t^{-}}\mathcal{W}2\mathcal{S}(\varphi_{1}).\text{ Since for
all }l\geq|\pi|:\pi,l\models_{t^{-}}\psi\text{ for each possible
}\psi:\dots\Leftrightarrow\forall j\geq
i:\pi,j\models_{t^{-}}\mathcal{W}2\mathcal{S}(\varphi_{2})\text{ or }\exists
k\geq i\text{ s.t.
}\pi,k\models_{t^{-}}\mathcal{W}2\mathcal{S}(\varphi_{2})\text{ and }\forall
i\leq
j<k:\pi,j\models_{t^{-}}\mathcal{W}2\mathcal{S}(\varphi_{1})\Leftrightarrow\pi,i\models_{t^{-}}G\mathcal{W}2\mathcal{S}(\varphi_{1})\vee\mathcal{W}2\mathcal{S}(\varphi_{1})U$
$\mathcal{W}2\mathcal{S}(\varphi_{2})\Leftrightarrow\pi,i\models_{t^{-}}\mathcal{W}2\mathcal{S}(\varphi_{2})R(\mathcal{W}2\mathcal{S}(\varphi_{1})\vee\mathcal{W}2\mathcal{S}(\varphi_{2}))$

##  4\. Compositional reasoning

###  4.1. Formal problem

Compositional verification proves the properties of a system by proving the
local properties on components and by checking that the composition of the
local properties satisfies the global one (see [RBH+01] for a generic
overview). This reasoning is expressed formally by inference 2, which is
parametrized by a function $\gamma_{S}$ that combines the components’
implementations and a related function $\gamma_{P}$ that combines the local
properties.

######  Inference 2.

Let $\mathcal{M}_{1},\mathcal{M}_{2},\dots,\mathcal{M}_{n}$ be a set of $n$
components, $\varphi_{1},\varphi_{2},\dots,\varphi_{n}$ be local properties on
each component, $\gamma_{S}$ is a function that defines the composition of
$\mathcal{M}_{1},\mathcal{M}_{2},\dots,\mathcal{M}_{n}$, $\gamma_{P}$ combines
the properties depending on the composition of $\gamma_{S}$ and $\varphi$ a
property. The following inference is true:
$\gamma_{S}(\mathcal{M}_{1},\mathcal{M}_{2},\dots,\mathcal{M}_{n})\models\varphi\lx@proof@logical@and\gamma_{S}(\mathcal{M}_{1},\mathcal{M}_{2},\dots,\mathcal{M}_{n})\models\gamma_{P}(\varphi_{1},\varphi_{2},\dots,\varphi_{n})\mathcal{M}_{1}\models\varphi_{1},\mathcal{M}_{2}\models\varphi_{2},\dots,\mathcal{M}_{n}\models\varphi_{n}\gamma_{P}(\varphi_{1},\varphi_{2},\dots,\varphi_{n})\models\varphi$

The problem we address in this paper is to define proper
$\gamma_{S},\gamma_{P}$ representing the composition of respectively ITS and
truncated properties such that the inference rule holds.

###  4.2. Interface Transition Systems

In this paper, we represent I/O components as Interface Transition Systems, a
symbolic version of interface automata [dAH01] that considers I/O variables
instead of I/O actions.

An Interface Transition System (ITS) $\mathcal{M}$ is a tuple
$\mathcal{M}=\langle V^{I},V^{O},\mathcal{I},\mathcal{T},\mathcal{SF}\rangle$
where:

  * •

$V_{I}$ is the set of input variables while $V_{O}$ is the set of output
variables where $V_{I}\cap V_{O}=\emptyset$.

  * •

$V:=V_{I}\cup V_{O}$ denotes the set of the variables of $\mathcal{M}$

  * •

$\mathcal{I}$ is the initial condition, a formula over $V_{O}$,

  * •

$\mathcal{T}$ is the transition condition, a formula over $V\cup
V_{O}^{\prime}$ where $V_{O}^{\prime}$ is the primed versions of $V_{O}$

  * •

$\mathcal{SF}$ is the set of strong fairness constraints, a set of pairs of
formulas over $V$.

A symbolic transition system with strong fairness $\mathcal{M}=\langle
V,\mathcal{I},\mathcal{T},\mathcal{SF}\rangle$ is an interface transition
system without input variables (i.e.,
$\langle\emptyset,V,\mathcal{I},\mathcal{T},\mathcal{SF}\rangle$).

A trace $\pi$ of an ITS $\mathcal{M}$ is a trace
$\pi=s_{0}s_{1}\dots\in\Pi(V^{I},V^{O})$ s.t.

  * •

$s_{0}\models\mathcal{I}$

  * •

For all $i<|\pi|-1$, $s_{i}\cup s_{i+1}^{\prime}\models\mathcal{T}$, and

  * •

If $\pi$ is infinite: for all $\langle f_{A},f_{G}\rangle\in\mathcal{SF}$, If
for all $i$ there exists $j\geq i$, $s_{j}\models f_{A}$ then for all $i$
there exists $j\geq i:s_{j}\models f_{G}$.

The finite (infinite) language $\mathcal{L}^{<\omega}(\mathcal{M})$
($\mathcal{L}^{\omega}(\mathcal{M})$)of an ITS $\mathcal{M}$ is the set of all
finite (infinite) traces of $\mathcal{M}$. Finally, we denote
$\mathcal{L}(\mathcal{M}):=\mathcal{L}^{<\omega}(\mathcal{M})\cup\mathcal{L}^{\omega}(\mathcal{M})$
as the language of $\mathcal{M}$.

Let $\pi=s_{0}s_{1}\dots$ be a trace of an ITS $\mathcal{M}$ and
$V^{\prime}\subseteq V$ a set of symbols of $\mathcal{M}$. We denote
$s_{i}(V^{\prime})$ as the restriction of the assignment $s_{i}$ to the
symbols of $V^{\prime}$; moreover, we denote
$\pi_{|V^{\prime}}:=s_{0}(V^{\prime})s_{1}(V^{\prime})\dots$ as the
restriction of all the state assignments of $\pi$ to the symbols of
$V^{\prime}$. Furthermore, we denote
$\mathcal{L}(\mathcal{M})_{|V^{\prime}}=\\{\pi_{|V^{\prime}}|\pi\in\mathcal{L}(\mathcal{M})\\}$
as the restriction of all the traces of the language of an ITS $\mathcal{M}$
to a set of symbols $V^{\prime}\subseteq V$. Let
$\mathcal{M}_{1},\dots,\mathcal{M}_{n}$ be $n$ ITS, they are said compatible
iff they share respectively only input with output (i.e. $\forall i\leq
n,j\leq n\text{ s.t. }i\neq j:V^{i}\cap V^{j}=(V^{i}_{O}\cap
V^{j}_{I})\cup(V^{i}_{I}\cap V^{o}_{O})$)

###  4.3. Asynchronous composition of ITS: $\gamma_{S}$

Let $\mathcal{M}_{1},\dots,\mathcal{M}_{n}$ be $n$ compatible interface
transition systems, let $run_{1},\dots,run_{n}$ be $n$ Boolean variables
variables not occurring in $\mathcal{M}_{1},\dots,\mathcal{M}_{n}$ and let
$end_{1},\dots,end_{n}$ be $n$ Boolean variables not occurring in
$\mathcal{M}_{1},\dots,\mathcal{M}_{n}$.
$\mathcal{M}_{1}\otimes\dots\otimes\mathcal{M}_{n}=\langle
V^{I},V^{O},\bigwedge_{1\leq i\leq
n}{\mathcal{I}_{i}},\mathcal{T},\mathcal{SF}\rangle$ where:

$\displaystyle V^{I}=$ $\displaystyle(\bigcup_{1\leq i\leq
n}{V^{I}_{i}\cup\\{run_{i}\\}})\setminus(\bigcup_{1\leq i<n}\bigcup_{i<j\leq
n}V_{i}\cap V_{j})$ $\displaystyle V^{O}=$ $\displaystyle(\bigcup_{1\leq i\leq
n}{V^{O}_{i}}\cup\\{end_{i}\\})\cup(\bigcup_{1\leq i<n}\bigcup_{i<j\leq
n}V_{i}\cap V_{j})$ $\displaystyle\mathcal{T}=$ $\displaystyle\bigwedge_{1\leq
i\leq
n}{((run_{i}\rightarrow\mathcal{T}_{i})\wedge\psi_{cond}^{\mathcal{M}_{i}}\wedge(end_{i}\leftrightarrow
end_{i}^{\prime}\wedge\neg run_{i}))}$ $\displaystyle\mathcal{SF}=$
$\displaystyle\bigcup_{1\leq i\leq n}(\\{\langle\top,run_{i}\vee
end_{i}\rangle\\}\cup\\{\langle
run_{i}\wedge\varphi_{a},run_{i}\wedge\varphi_{g}\rangle|\langle\varphi_{a},\varphi_{g}\rangle\in\mathcal{SF}_{i}\\})$

where $\psi_{cond}^{\mathcal{M}_{i}}:=\neg run_{i}\rightarrow\bigwedge_{v\in
V^{O}_{i}}{v=v^{\prime}}$. $\otimes$ provides a notion of asynchronous
composition of Interface Transition Systems based on interleaving. Each
component can either run (execute a transition) or stutter (freeze output
variables). Contrary to our previous work[BT22], this new definition allows
for finite executions of local components. For each $i$, we introduce the
variable $run_{i}$ representing the execution of a transition of
$\mathcal{M}_{i}$; furthermore, we introduce the prophecy variables $end_{i}$
that monitor whether or not a component will execute new transitions in the
future i.e. $end_{i}$ is equivalent to $G\neg run_{i}$.

Let $\pi$ be a trace of
$\mathcal{M}=\mathcal{M}_{1}\otimes\dots\otimes\mathcal{M}_{n}$ with $i\leq
n$. We define the projection function
$Pr_{\mathcal{M}_{i}}:\Pi(V)\rightarrow\Pi(V_{i})$ as follows:

$Pr_{\mathcal{M}_{i}}(\pi)=\begin{cases}s_{i_{0}}(V_{i}),\dots&\text{ If
}\pi\text{ is infinite and }\pi\models GFrun_{i}\\\
s_{i_{0}}(V_{i}),\dots,s_{i_{n-1}}(V_{i}),s_{i_{n}}(V^{O}_{i})&\text{
Otherwise }\end{cases}$

where $i_{k}$ is the sequence mapping each state of $\pi_{i}$ into a state of
$\pi$ as follows:

$i_{k}:=\begin{cases}k&\text{ If }k<0\\\ i_{k-1}+1&\text{ If }k\geq|\pi|-1\\\
k^{\prime}\mid k^{\prime}>i_{k-1},\pi,k^{\prime}\models run_{i}\text{ and
}\forall_{i_{k-1}<j^{\prime}<k^{\prime}}\pi,j^{\prime}\nvDash run_{i}&\text{
Otherwise}\end{cases}$

Moreover, we define the inverse operator of $Pr$, denoted by $Pr^{-1}$:

$Pr^{-1}_{\mathcal{M}_{i}}(\pi)=\\{\pi^{\prime}|Pr_{\mathcal{M}_{i}}(\pi^{\prime})=\pi\\}$

Definition 4.3 provides a mapping between the composed ITS and the local
transition system. A graphical representation of projection is shown in Figure
2. We now show that the language of each local ITS $\mathcal{M}_{i}$ contains
the language of the composition projected to the local ITS. From this result
we can derive a condition for $\gamma_{P}$ such that Inference 2 holds.

$\bar{s}_{j+0}$$\bar{s}_{j+1}$$\bar{s}_{j+2}$$\bar{s}_{j+3}$$\bar{s}_{j+4}$$\bar{s}_{j+5}$……$\pi$
$v_{i},\neg v_{o},\newline run_{i}$ $\neg v_{i},\neg v_{o},\newline \neg
run_{i}$ $\neg v_{i},\neg v_{o},\newline \neg run_{i}$ $v_{i},\neg
v_{o},\newline run_{i}$ $v_{i},v_{o},\newline \neg run_{i}$ $\neg
v_{i},v_{o},\newline run_{i}$ $s_{i+0}$$s_{i+1}$$s_{i+2}$……$\pi_{i}$
$v_{i},\neg v_{o}$$v_{i},\neg v_{o}$$\neg v_{i},v_{o}$ Figure 2. Graphical
view of trace projection. White states of $\pi$ represent the states of the
sequence $i_{i}$.

######  Theorem 3.

Let $\mathcal{M}=\mathcal{M}_{1}\otimes\dots\otimes\mathcal{M}_{n}$:

$\text{For all }1\leq i\leq
n:\mathcal{L}(\mathcal{M}_{i})\supseteq\\{Pr_{\mathcal{M}_{i}}(\pi)|\pi\in\mathcal{L}(\mathcal{M})\\}$

######  Proof 4.1.

Given a trace
$\pi\in\mathcal{L}(\mathcal{M}),\pi_{i}:=Pr_{\mathcal{M}_{i}}(\pi)$. We prove
the theorem by induction on the length of $\pi_{i}$. The inductive hypothesis
states that if $|\pi_{i}|>k+1$ and $\pi_{i}^{0\dots
k}\in\mathcal{L}^{<\omega}(\mathcal{M}_{i})$, then $\pi_{i}^{0\dots
k+1}\in\mathcal{L}^{<\omega}(\mathcal{M}_{i})$.

  * •

Base case:
By definition $\mathcal{I}:=\bigwedge_{1\leq i\leq n}\mathcal{I}_{i}$ and
$\pi_{i}(0)=\pi(i_{0})(V_{i})$. We derive that
$\pi_{i},0\models\mathcal{I}_{i}\Rightarrow\pi_{i}^{0\dots
0}\in\mathcal{L}^{<\omega}(\mathcal{M}_{i})$. It should be noted that this
holds also if $|\pi_{i}|=1$ and $\pi,|\pi|-1\nvDash run_{i}$ because
$\mathcal{I}_{i}$ is a proposition on symbols of $V^{O}_{i}$.

  * •

Inductive case:
By definition $\pi_{i}(k)=\pi(i_{k})(V_{i})$ where $i_{k}$ is the kth position
s.t. $run_{i}$ holds. Therefore, $\pi(i_{k})\pi(i_{k}+1)\models
run_{i}\rightarrow\mathcal{T}_{i}\Rightarrow\pi(i_{k})\pi(i_{k}+1)\models\mathcal{T}_{i}$.
By $\psi_{cond}^{\mathcal{M}_{i}}$ we obtain that
$\pi_{i_{k+1}}(V^{O}_{i})=\pi_{i_{k}+1}(V^{O}_{i})=\pi_{i}(k+1)(V^{O}_{i})$.
Since $\mathcal{T}_{i}$ reasons over symbols of $V\cup{V^{O}}^{\prime}$, then
$\pi(i_{k})\pi(i_{k}+1)\models\mathcal{T}_{i}\Leftrightarrow\pi_{i}(k)\pi_{i}(k+1)\models\mathcal{T}_{i}$.
Therefore, $\pi_{i},k\models\mathcal{T}_{i}$ which guarantees that
$\pi_{i}^{0\dots k+1}\in\mathcal{L}^{<\omega}(\mathcal{M}_{i})$.

We proved the theorem for finite traces, we now extend the proof to consider
infinite traces. To do so, it is sufficient to prove that each infinite trace
$\pi_{i}$ satisfies the strong fairness conditions of $\mathcal{SF}_{i}$ since
it already satisfies $\mathcal{I}_{i}$ and $\mathcal{T}_{i}$.

Since $\pi_{i}=Pr_{\mathcal{M}_{i}}(\pi)$ and
$\pi\in\mathcal{L}(\mathcal{M})$, $\pi\models\bigwedge_{\langle
f_{a},f_{g}\rangle\in\mathcal{SF}}(GFf_{a}\rightarrow GFf_{g})$. In
particular, due to the composition, $\pi\models\bigwedge_{\langle
f_{a},f_{g}\rangle\in\mathcal{SF}_{i}}(GF(run_{i}\wedge f_{a})\rightarrow
GF(run_{i}\wedge f_{g}))$ The projection defines the sequence $i_{0},\dots$
representing the points in which $run_{i}$ holds; therefore, for all $\langle
f_{a},f_{g}\rangle\in$if for all $k$ there exists $j\geq k$ s.t.
$\pi,i_{k}\models f_{a}$ then for all $k^{\prime}$ there exists
$j^{\prime}\geq k^{\prime}$ s.t. $\pi,i_{k}^{\prime}\models f_{g}$. From the
projection definition then $\pi_{i}\models GFf_{a}\rightarrow GFf_{g}$ for
each $\langle f_{a},f_{g}\rangle\in\mathcal{SF}_{i}$.

Let $\mathcal{M}_{1},\dots,\mathcal{M}_{n}$ be $n$ ITS, we define $\gamma_{S}$
as follows:

$\gamma_{S}(\mathcal{M}_{1},\dots,\mathcal{M}_{n}):=\mathcal{M}_{1}\otimes\dots\otimes\mathcal{M}_{n}$

To complete our compositional reasoning, we need to define the function
$\gamma_{P}$ such that Inference 2 holds. To do so, Section 5 provides a
rewriting technique that maps each local trace satisfying $\varphi_{i}$ to a
global trace satisfying $\gamma_{P}$.

##  5\. Rewriting

In this section, we introduce a rewriting-based approach for the composition
of local properties. In section 5.1, we present the rewriting of the
propositional part of the logic of Section 3 that maps local properties to
global properties. In section 5.2, we extend the rewriting to all the
operators of out logic and we prove the lemmas and the theorem of our
rewriting. In section 5.3, we propose an optimized version of the rewriting.
Finally, in section 5.4, we propose a variation of the optimized rewriting
tailored for infinite executions of local properties i.e. in which the
semantics is the one of standard LTL because we assume fairness of $run_{i}$.

To simplify the notation, we assume to be given $n$ interface transition
systems $\mathcal{M}_{1},\dots,\mathcal{M}_{n}$, a composed ITS
$\mathcal{C}=\mathcal{M}_{1}\otimes\dots\otimes\mathcal{M}_{n}$, a trace $\pi$
of $\mathcal{M}_{i}$ with $i<n$, a local property $\varphi$ and a local term
$u$. For brevity, we refer to $\mathcal{R}_{\mathcal{M}_{i}}$,
$\mathcal{R}^{*}_{\mathcal{M}_{i}}$,
${\mathcal{R}^{\theta}}_{\mathcal{M}_{i}}$, $Pr^{-1}_{\mathcal{M}_{i}}$,
$Pr_{\mathcal{M}_{i}}$, $end_{i}$ and $run_{i}$ as respectively
$\mathcal{R},\mathcal{R}^{*},{\mathcal{R}^{\theta}},{\mathcal{R}^{\theta}}^{*},Pr^{-1},Pr,end\text{
and }run$. Moreover, we will refer to $i_{0},i_{1},\dots$ as the sequence of
definition 4.3. As in section 3.2, we denote input predicates with apex $I$:
$Pred^{I}$ and the output predicates and terms with apex $O$: $Pred^{O}$.
Finally, we denote $sgn\in\\{-,+\\}$.

###  5.1. Propositional LTL compositional rewriting

In this section, we propose a rewriting to asynchronously compose
propositional truncated LTL properties over Interface Transition Systems
symbols.

The idea is based on the notions of projection (introduced in Definition 4.3)
and asynchronous composition (introduced in Definition 4.3). We produce a
rewriting $\mathcal{R}^{*}$ for $\varphi$ such that each trace $\pi$ of
$\mathcal{M}_{i}$ satisfies the rewritten formula iff the projected trace
satisfies the original property.

We define $\mathcal{R}$ as the following rewriting function:

$\displaystyle\mathcal{R}^{-}(Pred^{I}(u_{1},\dots,u_{n})):=\neg run\vee
Pred^{I}(\mathcal{R}^{-}(u_{1}),\dots,\mathcal{R}^{-}(u_{n}))$
$\displaystyle\mathcal{R}^{+}(Pred^{I}(u_{1},\dots,u_{n})):=run\wedge
Pred^{I}(\mathcal{R}^{+}(u_{1}),\dots,\mathcal{R}^{+}(u_{n}))$
$\displaystyle\mathcal{R}^{sgn}(Pred^{O}(u_{1},\dots,u_{n})):=Pred^{O}(\mathcal{R}^{sgn}(u_{1}),\dots,\mathcal{R}^{sgn}(u_{n}))$
$\displaystyle\mathcal{R}^{sgn}(\varphi_{1}\vee\varphi_{2}):=\mathcal{R}^{sgn}(\varphi_{1})\vee\mathcal{R}^{sgn}(\varphi_{2})$
$\displaystyle\mathcal{R}^{-}(\neg\varphi):=\neg\mathcal{R}^{+}(\varphi),\mathcal{R}^{+}(\neg\varphi):=\neg\mathcal{R}^{-}(\varphi)$
$\displaystyle\mathcal{R}^{-}(X\varphi):=X(stateR(\neg
state\vee\mathcal{R}^{-}(\varphi)))$
$\displaystyle\mathcal{R}^{+}(X\varphi):=X(\neg
stateU(state\wedge\mathcal{R}^{+}(\varphi)))$
$\displaystyle\mathcal{R}^{-}(\varphi_{1}U\varphi_{2}):=(\neg
state\vee\mathcal{R}^{-}(\varphi_{1}))U(state\wedge\mathcal{R}^{-}(\varphi_{2})\vee
Yend)$ $\displaystyle\mathcal{R}^{+}(\varphi_{1}U\varphi_{2}):=(\neg
state\vee\mathcal{R}^{+}(\varphi_{1}))U(state\wedge\mathcal{R}^{+}(\varphi_{2}))$

where $state:=run\vee Zrun\wedge end$ and
$\mathcal{R}(\varphi)=\mathcal{R}^{-}(\varphi)$ $\mathcal{R}$ transform the
formula applying $run$ and $state$ to $\varphi$. The general intuition is that
when $run$ is true, the local component triggers a transition. Moreover,
$state$ represents a local state of $\pi$ in the global trace. It should be
noted that the rewriting have to deal with the last state. Therefore, $state$
is represented by a state that either satisfies $run$ or is the successor of
the last state that satisfies $run$.

######  Lemma 4.

For all $\pi^{ST}\in Pr^{-1}(\pi)$, for all $i<|\pi|$:

$\displaystyle\pi,i\models_{t^{sgn}}\varphi\Leftrightarrow\pi^{ST},i_{i}\models_{t^{sgn}}\mathcal{R}^{sgn}(\varphi)$

######  Proof 5.1.

Proofs can be found in Section 5.2.1.

Lemma 4 states that each point in the sequence $i_{0},\dots$ of $\pi^{ST}$
satisfies $\mathcal{R}(\varphi)$ iff the local property satisfies in that
point $\varphi$; therefore, providing a mapping between the two properties.

For output predicates, the rewriting is transparent because the projection
definition guarantees that each state $i$ of $\pi$ has the same evaluation of
each $i_{i}$ state of $\pi^{ST}$. Although this holds for input predicates as
well, there is a semantic technicality that should be taken into account.
Input predicates are evaluated differently on the last state: with strong
semantics ($+$) they do not hold while on weak semantics ($-$) they hold.
Therefore, with strong semantics, the rewriting forces the predicate to hold
in a transition i.e. when $run$ holds. The weak semantics is managed
specularly.

Regarding $X$, $\mathcal{R}^{-}$ needs to pass from point $i_{i}$ to $i_{i+1}$
and to verify that the sub-formula is verified in that state. The first $X$
passes from $i_{i}$ to $i_{i}+1$. Then, the rewriting skips all states that
are not $i_{i+1}$ and ”stops” in position $i_{i+1}$. Figure 3 shows an
intuitive representation of the rewriting of $X$.

For until formulae, the rewriting needs to ”skip” all points that either do
not belong to the local trace or satisfy the left part of the formula while it
must ”stop” to a point that satisfies the right part and is a state in the
local trace. To do so, it introduces a disjunction with $state$ on the left
side of the formula and a conjunction with $state$ on the right side of the
formula. Figure 4 shows an intuitive representation of the rewriting of $U$.

$s_{i+0}$$\bar{s}_{j+0}$$\bar{s}_{j+1}$$\bar{s}_{j+2}$$\bar{s}_{j+3}$$\bar{s}_{j+4}$……$\pi^{ST}$
$a,run$$\neg a,\neg run$$\neg a,\neg run$$a,run$$\neg
a,run$$s_{i+1}$$s_{i+2}$……$\pi$ $a$$a$$\neg a$$a$$Xa$$\neg run\vee
a$$run\wedge a$$stateR(\neg state\vee a)$$\mathcal{R}^{-}(Xa)$ Figure 3.
Graphical representation of rewriting of $X$
$s_{i+0}$$\bar{s}_{j+0}$$\bar{s}_{j+1}$$\bar{s}_{j+2}$$\bar{s}_{j+3}$$\bar{s}_{j+4}$……$\pi^{ST}$
$a,\neg b,run$$\neg a,b,\neg run$$\neg a,\neg b\neg run$$a,\neg b,run$$\neg
a,b,run$$s_{i+1}$$s_{i+2}$……$\pi$ $a,\neg b$$a,\neg b$$\neg
a,b$$b$$a$$aUb$$\neg state\vee a$$state\wedge b$$\mathcal{R}^{-}(aUb)$ Figure
4. Graphical representation of rewriting of $U$

We define $\mathcal{R}^{*}$ as $\mathcal{R}^{*}(\varphi):=stateR(\neg
state\vee\mathcal{R}(\varphi))$.

######  Lemma 5.

For all $\pi^{ST}\in
Pr^{-1}(\pi)\pi^{ST},i_{0}\models_{t}\mathcal{R}^{sgn}(\varphi)\Leftrightarrow\pi^{ST},0\models_{t}\mathcal{R}^{*}(\varphi)$

######  Proof 5.2.

Proofs can be found in Section 5.2.1.

Lemma 4 shows that $\mathcal{R}$ guarantees that satisfiability is preserved
in the active transitions of the global traces. However, $i_{0}$ is not always
granted to be equal to $0$ (see definition 4.3), and thus, we need to find a
rewriting that guarantees that satisfiability is preserved in the first
transition as well. From lemma 4 and lemma 5, we infer the rewriting theorem.
The theorem maps the local trace to the global trace as follows:

######  Theorem 6.

For all $\pi^{ST}\in
Pr^{-1}(\pi):\pi\models_{t}\varphi\Leftrightarrow\pi^{ST}\models_{t}\mathcal{R}^{*}(\varphi)$

######  Proof 5.3.

Proofs can be found in Section 5.2.1.

###  5.2. Complete LTL rewriting

We extend the rewriting $\mathcal{R}$ with the rewriting of the remaining
operators:

$\displaystyle\mathcal{R}^{sgn}(Y\varphi):=Y(\neg
runS(run\wedge\mathcal{R}^{sgn}(\varphi)))$
$\displaystyle\mathcal{R}^{sgn}(\varphi_{1}S\varphi_{2}):=(\neg
state\vee\mathcal{R}^{sgn}(\varphi_{1}))S(state\wedge\mathcal{R}^{sgn}(\varphi_{2}))$
$\displaystyle\mathcal{R}^{sgn}(func(u_{1},...,u_{n})):=func(\mathcal{R}^{sgn}(u_{1}),...,\mathcal{R}^{sgn}(u_{n}))$
$\displaystyle\mathcal{R}^{sgn}(x):=x,\mathcal{R}^{sgn}(c):=c$
$\displaystyle\mathcal{R}^{sgn}(ite(\varphi,u_{1},u_{2})):=ite(\mathcal{R}^{+}(\varphi),\mathcal{R}^{-}(u_{1}),ite(\mathcal{R}^{+}(\neg
u_{2}),\mathcal{R}^{-}(u_{2}),def_{ite(\varphi,u_{1},u_{2})}))$
$\displaystyle\mathcal{R}^{sgn}(u@\tilde{F}\varphi):=\mathcal{R}^{sgn}(u)@\tilde{F}(state\wedge\mathcal{R}^{+}(\varphi))$
$\displaystyle\mathcal{R}^{sgn}(u@\tilde{P}\varphi):=\mathcal{R}^{sgn}(u)@\tilde{P}(state\wedge\mathcal{R}^{+}(\varphi))$

######  Example 5.4.

Consider the formula $\varphi_{c2}:=G(rec_{2}\rightarrow
out_{2}^{\prime}=in_{2}\wedge Xsend_{2})$ from Figure 1. The rewriting
$\mathcal{R}^{*}(\varphi_{c2})$ is defined as the following formula.

$G(\neg state\vee(\underbrace{run\wedge
rec_{2}}_{\mathcal{R}^{+}(rec_{2})}\rightarrow\overbrace{out_{2}@\tilde{F}state=in_{2}}^{\mathcal{R}(out_{2}@\tilde{F}\top)}\wedge\underbrace{X(runR(\neg
run\vee send_{2}))}_{\mathcal{R}(Xsend_{2})}))$

Finally, $\mathcal{R}^{*}(\varphi_{c2})$ is defined as $stateR(\neg
state\vee\mathcal{R}^{-}(\varphi_{c2})$.

####  5.2.1. $\mathcal{R}^{*}$ proofs

######  Proof 5.5.

We prove Lemma 4 by induction on the formula. Before starting the proof we
observe the following facts:

  1. (1)

For all $i:i<|\pi|-1\Leftrightarrow\pi^{ST},i_{i}\models_{t^{+}}run$.

  2. (2)

For all $i:i<|\pi|\Leftrightarrow\pi^{ST},i_{i}\models_{t^{+}}state$.

  3. (3)

$\forall i<|\pi|,\forall i_{i-1}<j\leq
i_{i}:\pi^{ST},i_{i}\models_{t^{-}}\psi\Leftrightarrow\pi^{ST},j\models_{t^{-}}stateR(\neg
state\vee\psi)$.

  4. (4)

$\forall i<|\pi|,\forall i_{i-1}<j\leq
i_{i}:\pi^{ST},i_{i}\models_{t^{+}}\psi\Leftrightarrow\pi^{ST},j\models_{t^{+}}\neg
stateU(state\wedge\psi)$.

  5. (5)

$\pi^{ST},i_{|\pi|-1}+1\models_{t^{sgn}}Yend$ .

Base cases:

  * •

$Pred^{I}$: $\pi,i\models_{t^{-}}Pred^{\mathcal{I}}\Leftrightarrow
i\geq|\pi|-1\vee
Pred^{\mathcal{I}}\overset{Pr}{\Leftrightarrow}i\geq|\pi|-1\text{ or
}\pi^{ST},i_{i}\models_{t^{-}}Pred^{I}\overset{\ref{itm:run}}{\Leftrightarrow}\pi^{ST},i_{i}\models_{t^{-}}\neg
run\vee Pred^{\mathcal{I}}$. The strong semantics case is identical.

  * •

$Pred^{0},x,c$: Trivial.

Inductive cases:

  * •

$\neg$: Trivial in both cases. It follows the semantics definition

  * •

$\vee,Pred^{I},Pred^{O},func$: Trivial.

  * •

$X\varphi:\pi^{ST},i_{i}\models_{t^{-}}\mathcal{R}(X\varphi)\Leftrightarrow\pi^{ST},i_{i}+1\models_{t^{-}}stateR(\neg
state\vee\mathcal{R}(\varphi))\overset{\ref{itm:weak}}{\Leftrightarrow}\pi^{ST},i_{i+1}\models_{t^{-}}\mathcal{R}(\varphi)$
if $i<|\pi|-1$ (By ind. holds). Otherwise, $i=|\pi|-1$ and thus
$\pi^{ST},i_{i}+1\models_{t^{-}}G\neg run$ which implies
$\pi^{ST},i_{i}\models\mathcal{R}(X\varphi)$ as expected by the weak
semantics. We skip the strong case because it is similar.

  * •

$\varphi_{1}U\varphi_{2}:\pi^{ST},i_{i}\models_{t^{-}}\mathcal{R}^{-}(\varphi_{1}U\varphi_{2})\Leftrightarrow\pi^{ST},\models_{t^{-}}i_{i}(state\vee\mathcal{R}^{-}(\varphi_{1}))U(\neg
state\wedge\mathcal{R}^{-}(\varphi_{2})\vee Yend)\Leftrightarrow\exists
k^{\prime}\geq i_{i}\text{ s.t.
}(\pi^{ST},k^{\prime}\models_{t^{-}}\mathcal{R}^{-}(\varphi_{2})\text{ and
}\pi^{ST},k^{\prime}\models_{t^{-}}state\text{ or
}\pi^{ST},k^{\prime}\models_{t^{-}}Yend)\text{ and }\forall i_{i}\leq
j^{\prime}<k^{\prime}:\pi^{ST},j^{\prime}\models_{t^{-}}\mathcal{R}(\varphi_{1})\text{
or
}\pi^{ST},j^{\prime}\models_{t^{-}}state\overset{\ref{itm:state},\ref{itm:ye}}{\Leftrightarrow}\exists
k\geq i\text{ s.t.
}\pi^{ST},i_{k}\models_{t^{-}}\mathcal{R}(\varphi_{2})\text{ and
}k<|\pi|\text{ or }k=|\pi|\text{ and }\forall i\leq
j<k\pi^{ST},i_{j}\models_{t^{-}}\mathcal{R}(\varphi_{1})\overset{Ind.(k,j<|\pi|),\forall\phi:\pi,|\pi|\models_{t^{-}}\phi}{\Leftrightarrow}\exists
k\geq i\text{ s.t. }\pi,k\models_{t^{-}}\varphi_{2}\text{ and }\forall i\leq
j<k:\pi,j\models_{t^{-}}\varphi_{1}\Leftrightarrow\pi,i\models_{t^{-}}\varphi_{1}U\varphi_{2}$.
The proof of the strong case is the same.

  * •

$Y\varphi$: The case is specular to the case of $X$. In this specific case, we
can use $run$ instead of $state$ because we are assuming that $i<|\pi|$;
therefore
$i-1<|\pi|-1\overset{\ref{itm:run}}{\Rightarrow}\pi^{ST},i_{i-1}\models_{t^{-}}run$
(if $i=0$, then property is false).

  * •

$\varphi_{1}S\varphi_{2}:$ The case is specular to $U$. It is sufficient to
observe that 4 can be applied for the past as well.

  * •

$ite(\varphi,u_{1},u_{2}):\pi^{ST}(i_{i})(\mathcal{R}^{sgn}(ite(\varphi,u_{1},u_{2})))=\pi^{ST}(i_{i})(\mathcal{R}^{-}(u_{1}))\text{
If
}\pi^{ST},i_{i}\models_{t^{+}}\varphi;\dots=\pi^{ST}(i_{i})(\mathcal{R}^{-}(u_{2}))\text{
If
}\pi^{ST},i_{i}\models_{t^{+}}\neg\varphi;\dots=\pi^{ST}(def_{ite(\varphi,u_{1},u_{2})})\text{
Otherwise}$. By induction the case holds.

  * •

$u@\tilde{F}\varphi:\pi^{ST}(i_{i})(\mathcal{R}^{sgn}(u@\tilde{F}\varphi))=\pi^{ST}(i_{i})(\mathcal{R}^{-}(u)@\tilde{F}(state\wedge\mathcal{R}^{+}(\varphi))):\pi^{ST}(i_{i})(\dots)=\pi^{ST}(j)(\mathcal{R}^{-}(u))\text{
if }\exists j>i_{i}\text{ s.t. }\pi^{ST},j\models_{t^{+}}state\text{ and
}\pi^{ST},j\models_{t^{+}}\mathcal{R}^{+}(\varphi)$;
$\pi^{ST}(i_{i})(\dots)=def_{u@\tilde{F}\varphi}\text{
otherwise.}\pi^{ST}(i_{i})(\dots)\overset{\ref{itm:state}}{=}\pi^{ST}(i_{j})(\mathcal{R}^{-}(u))\text{
if }\exists j\geq i\text{ s.t.
}\pi^{ST},i_{j}\models_{t^{+}}\mathcal{R}^{+}(\varphi);\pi^{ST}(i_{i})(\dots)=def_{\dots}$
otherwise. Finally, by induction hypothesis, the case is proved.

  * •

$u@\tilde{P}\varphi:$ Identical to $@\tilde{F}$.

Additionally, we prove Lemma 5 by simply applying observation 3.

######  Proof 5.6.

We prove Theorem 6 through Lemma 4 and Lemma 5:

By Lemma 4, $\forall
i:\pi,i\models_{t^{sgn}}\varphi\Leftrightarrow\pi^{ST},i_{i}\models_{t^{sgn}}\mathcal{R}^{sgn}(\varphi)$.
Therefore,
$\pi\models_{t^{-}}\varphi\Leftrightarrow\pi^{ST},i_{0}\models_{t^{-}}\mathcal{R}^{-}(\varphi)$.
By Lemma 5,
$\pi^{ST},i_{0}\models_{t^{sgn}}\mathcal{R}^{-}(\varphi)\Leftrightarrow\pi^{ST}\models_{t^{sgn}}\mathcal{R}^{*}(\varphi)$.
Therefore,
$\pi\models_{t^{-}}\varphi\Leftrightarrow\pi^{ST}\models_{t^{-}}\mathcal{R}^{*}(\varphi)$.

###  5.3. Optimized LTL compositional rewriting

The main weakness of the rewriting proposed in previous sections is the size
of the resulting formula. However, there are several cases in which it is
possible to apply a simpler rewriting. For instance, $Gv_{o}$ is rewritten by
$\mathcal{R}^{sgn}$ into $G(\neg state\vee v_{o})$ while by $\psi_{cond}$ (see
Definition 4.3) it does not need to be rewritten since output variables do not
change when $run$ is false. Similarly, $Xv_{o}$ can be rewritten in the weak
semantics to $end\vee Xv_{o}$.

To do so, we apply the concept of stutter-tolerance introduced in [BT22]
tailored for possibly finite traces. Informally, a formula is said stutter-
tolerant if it keeps the same value when rewritten with $\mathcal{R}^{sgn}$ in
all adjacent stuttering transitions.

An LTL formula $\varphi$ and a term $u$ are respectively said stutter-tolerant
w.r.t. $\mathcal{R}^{sgn}$ iff:
$\text{For all }\pi,\text{for all }\pi^{ST}\in Pr^{-1}(\pi),\text{for all
}0\leq i<|\pi|:\text{for all }{i_{i-1}<j<i_{i}}:$

$\displaystyle\pi^{ST},j\models_{t^{sgn}}\mathcal{R}^{sgn}(\varphi)\Leftrightarrow$
$\displaystyle\pi^{ST},i_{i}\models_{t^{sgn}}\mathcal{R}^{sgn}(\varphi)\text{
and }$ $\displaystyle\pi^{ST}(j)(\mathcal{R}^{sgn}(u))=$
$\displaystyle\pi^{ST}(i_{i})(\mathcal{R}^{sgn}(u))$

An LTL formula $\varphi_{st}$ is syntactically stutter-tolerant iff it has the
following grammar:

$\displaystyle\varphi_{st}:=$
$\displaystyle\varphi_{st}\vee\varphi_{st}\mid\neg\varphi_{st}\mid
Pred^{O}(u,\dots,u)\mid\varphi U\varphi\mid Y\varphi$ $\displaystyle u_{st}:=$
$\displaystyle func(u_{st},\dots,u_{st})\mid s\mid c\mid
ite(\varphi_{st},u_{st},u_{st})\mid u@\tilde{P}\varphi$

where $\varphi$ is an LTL formula, $u$ is a term from LTL syntax, $s$ is an
output variable and $c$ is a constant.

######  Lemma 7.

Syntactically stutter-tolerant formulas are stutter-tolerant w.r.t.
$\mathcal{R}^{sgn}$

######  Proof 5.7.

We prove the Lemma by induction on the size of the formula.

The base case is trivial since output variables remain unchanged during
stuttering. The inductive case is proved as follows:

  * •

$\vee,Pred^{O}$ and $\neg$: Trivial.

  * •

$U$: We can prove the correctness by induction on $j$, with base case
$j=i_{i}-1$. $\pi^{ST},j\models_{t^{-}}(\neg
state\vee\mathcal{R}^{-}(\varphi_{1}))U(state\wedge\mathcal{R}^{-}(\varphi_{2})\vee
end)\Leftrightarrow\pi^{ST},j\models_{t^{-}}(\mathcal{R}^{-}(\varphi_{2})\wedge
state\vee end)\vee(\neg state\vee\mathcal{R}^{-}(\varphi_{1}))\wedge X((\neg
state\vee\mathcal{R}^{-}(\varphi_{1})U(state\wedge\mathcal{R}^{-}(\varphi_{2})))\overset{\pi^{ST},j\nvDash_{t}state}{\Leftrightarrow}\pi^{ST},j\models_{t^{-}}X((\mathcal{R}^{-}(\varphi_{1})\vee\neg
state)U(state\wedge\mathcal{R}^{-}(\varphi_{2})\vee
end)\overset{j<|\pi^{ST}|-1}{\Leftrightarrow}\pi^{ST},j+1\models_{t^{-}}\mathcal{R}^{-}(\varphi_{1}U\varphi_{2})$
which is $i_{i}$ for the base case. The inductive case follows trivially.

  * •

$Y$: The case of $Y$ can be prove in the same way of $U$ by expanding $S$
instead of $U$.

  * •

$@\tilde{P}$: The semantics of at last evaluates $\mathcal{R}^{+}(\varphi)$ at
the first occurrence in the past of $state$. The proof is the same as $Y$.

From the notion of stutter tolerant formula, we provide an optimized rewriting
that is semantically equivalent to $\mathcal{R}^{sgn}$. If the sub-formulas of
$\varphi$ are syntactically stutter tolerant, we can simplify the rewriting
for $\varphi$.

We define ${\mathcal{R}^{\theta}}$ as follows. We omit the cases that are
identical to $\mathcal{R}$.

$\displaystyle{{\mathcal{R}^{\theta}}}^{-}(X\varphi):=end\vee
X{{\mathcal{R}^{\theta}}}^{-}(\varphi)\quad\text{ If }\varphi\text{ is synt.
st.tol.}$ $\displaystyle{{\mathcal{R}^{\theta}}}^{+}(X\varphi):=\neg end\wedge
X{{\mathcal{R}^{\theta}}}^{+}(\varphi)\quad\text{ If }\varphi\text{ is synt.
st.tol.}$
$\displaystyle{{\mathcal{R}^{\theta}}}^{-}(\varphi_{1}U\varphi_{2}):={{\mathcal{R}^{\theta}}}^{-}(\varphi_{1})U(Yend\vee{{\mathcal{R}^{\theta}}}^{-}(\varphi_{2}))\quad\text{
If }\varphi_{1}\text{ and }\varphi_{2}\text{ are synt. st. tol.}$
$\displaystyle{{\mathcal{R}^{\theta}}}^{+}(\varphi_{1}U\varphi_{2}):={{\mathcal{R}^{\theta}}}^{+}(\varphi_{1})U(\neg
Yend\wedge{{\mathcal{R}^{\theta}}}^{+}(\varphi_{2}))\quad\text{ If
}\varphi_{1}\text{ and }\varphi_{2}\text{ are synt. st. tol.}$
$\displaystyle{{\mathcal{R}^{\theta}}}^{sgn}(u@\tilde{F}\varphi):={{\mathcal{R}^{\theta}}}^{sgn}(u)@\tilde{F}({{\mathcal{R}^{\theta}}}^{sgn}(\varphi)\wedge\neg
end)\quad\text{ If }\varphi\text{ is synt. st. tol.}$

######  Lemma 8.

For all $\pi$, for all $\pi^{ST}\in Pr^{-1}(\pi)$, for all $i<|\pi|$:

$\displaystyle\pi,i\models_{t^{sgn}}\varphi\Leftrightarrow\pi^{ST},i_{i}\models_{t^{sgn}}{\mathcal{R}^{\theta}}(\varphi)$
$\displaystyle\pi(i)(u)=\pi^{ST}(i_{i})({\mathcal{R}^{\theta}}(u))$

######  Proof 5.8.

From Lemma 4, we deduce that to prove the Lemma it suffices to prove that
$\forall_{0\leq
i<|\pi|}\pi^{ST},i_{i}\models_{t^{sgn}}\mathcal{R}(\varphi)\Leftrightarrow\pi^{ST},i_{i}\models_{t^{sgn}}{\mathcal{R}^{\theta}}(\varphi)$
and
$\pi^{ST}(i_{i})(\mathcal{R}^{sgn}(u))=\pi^{ST}(i_{i})({{\mathcal{R}^{\theta}}}^{sgn}(u))$.
To prove that, we also prove inductively that if $\varphi$ is synt. st. tol.,
then $\forall_{0\leq
i<|\pi|}\forall_{i_{i-1}<j<i_{i}}\pi^{ST},j\models_{t^{sgn}}{{\mathcal{R}^{\theta}}}^{sgn}(\varphi)\Leftrightarrow\pi^{ST},i_{i}\mathcal{R}^{sgn}(\varphi)$.

We need to prove only the cases in which the sub-formulae are stutter tolerant
w.r.t $\mathcal{R}^{*}$.

  * •

$X$: If $end$ is true, then $i>=|\pi|-1$. Therefore, with weak semantics, the
formula shall be true while with strong semantics the formula shall be false.

If $end$ is false, then
$\pi^{ST},i_{i}\models_{t^{sgn}}{{\mathcal{R}^{\theta}}}^{sgn}(X\varphi)\Leftrightarrow\pi^{ST},i_{i}\models_{t^{sgn}}X{{\mathcal{R}^{\theta}}}^{sgn}(\varphi)\Leftrightarrow\pi^{ST},i_{i}+1\models_{t^{sgn}}{{\mathcal{R}^{\theta}}}^{sgn}(\varphi)$.
By induction hypothesis
$\dots\Leftrightarrow\pi^{ST},i_{i}+1\models_{t^{sgn}}\mathcal{R}(\varphi)\Leftrightarrow\pi^{ST},i_{i+1}\models_{t^{sgn}}\mathcal{R}(\varphi)$.

  * •

$U$:
$\pi^{ST},i_{i}\models_{t^{-}}{{\mathcal{R}^{\theta}}}^{-}(\varphi_{1})U(Yend\vee{{\mathcal{R}^{\theta}}}^{-}(\varphi_{2}))\Leftrightarrow\exists
k^{\prime}\geq i_{i}\text{ s.t. }\pi^{ST},k^{\prime}\models_{t^{-}}Yend\text{
or
}\pi^{ST},k^{\prime}\models_{t^{-}}{{\mathcal{R}^{\theta}}}^{-}(\varphi_{2})$
and $\forall_{i_{i}\leq
j^{\prime}<k^{\prime}}\pi^{ST},j^{\prime}\models_{t^{-}}{{\mathcal{R}^{\theta}}}^{-}(\varphi_{1})$.
By induction hypothesis $\exists i_{k}\geq i_{i}\text{ s.t.
}\pi^{ST},i_{k}\models_{t^{-}}\mathcal{R}(\varphi_{2})\text{ and
}\forall_{i_{i}\leq
i_{j}<i_{k}}\pi^{ST},i_{j}\models_{t^{-}}\mathcal{R}(\varphi_{1})$.

We now prove the additional part of the Lemma. If $\varphi_{1}$ or
$\varphi_{2}$ are not syntactically stutter tolerant, then the rewriting is
identical and thus, the lemma holds since $\varphi$ is stutter tolerant.

If $\varphi_{1}$ and $\varphi_{2}$ are syntactic stutter tolerant,
$\pi^{ST},j\models_{t^{-}}{{\mathcal{R}^{\theta}}}^{-}(\varphi_{1})U(Yend\vee{{\mathcal{R}^{\theta}}}^{-}(\varphi_{2}))\Leftrightarrow\exists
k^{\prime}\geq i_{i}\text{ s.t. }\pi^{ST},k^{\prime}\models_{t^{-}}Yend\text{
or
}\pi^{ST},k^{\prime}\models_{t^{-}}{{\mathcal{R}^{\theta}}}^{-}(\varphi_{2})$
and $\forall_{i_{i}\leq
j^{\prime}<k^{\prime}}\pi^{ST},j^{\prime}\models_{t^{-}}{{\mathcal{R}^{\theta}}}^{-}(\varphi_{1})$.
We observe that $\pi^{ST},k^{\prime}\models_{t^{-}}Yend\Leftrightarrow
k^{\prime}>i_{|\pi|-1}$. Moreover, by induction hypothesis, each $j^{\prime}$
and each $k^{\prime}$ can be replaced with respectively $i_{j}$ and $i_{k}$
s.t. $i\leq k\leq|\pi|$ and $i\leq j<k$. Therefore,
$\dots\Leftrightarrow\exists k\geq i\text{ s.t.
}\pi^{ST},i_{k}\models_{t^{-}}\mathcal{R}(\varphi_{2})$ or $k=|\pi|$ and
$\forall i\leq
j<k:\pi^{ST},i_{j}\models_{t^{-}}\mathcal{R}(\varphi_{1})\Leftrightarrow\pi,i\models_{t^{-}}\varphi_{1}U\varphi_{2}$.

  * •

$@\tilde{F}$: It follows from induction hypothesis and by Lemma 4

We define ${{\mathcal{R}^{\theta}}}^{*}$ as follows:

${{\mathcal{R}^{\theta}}}^{*}(\varphi):=\begin{cases}{{\mathcal{R}^{\theta}}}^{-}(\varphi)&\text{
If }\varphi\text{ is synt. st.tol.}\\\ stateR(\neg
state\vee{{\mathcal{R}^{\theta}}}^{-}(\varphi))&\text{ Otherwise}\end{cases}$

######  Lemma 9.

For all $\pi^{ST}\in
Pr^{-1}(\pi):\pi^{ST},i_{0}\models_{t}{\mathcal{R}^{\theta}}(\varphi)\Leftrightarrow\pi^{ST},0\models_{t}{\mathcal{R}^{\theta}}^{*}(\varphi)$

######  Proof 5.9.

If $\varphi$ is not syntactically stutter tolerant, then the proof is the same
one of lemma 5.

If $\varphi$ is syntactically stutter tolerant, then
$\forall_{i_{-1}<j<i_{i}}\pi^{ST},j\models_{t^{-}}{{\mathcal{R}^{\theta}}}^{-}(\varphi)\Leftrightarrow\pi^{ST},i_{0}\models_{t^{-}}{{\mathcal{R}^{\theta}}}^{-}(\varphi)$.
Since $i_{-1}$ is $-1$, then either $i_{0}=0$ or $j$ gets the value $0$ in the
for all; thus, proving the lemma.

######  Theorem 10.

For all $\pi^{ST}\in
Pr^{-1}(\pi):\pi\models_{t}\varphi\Leftrightarrow\pi^{ST}\models_{t}{\mathcal{R}^{\theta}}^{*}(\varphi)$

######  Proof 5.10.

The proof is identical to the proof of Theorem 6 using Lemma 8 and Lemma 9.

Theorem 6 and Theorem 10 show that respectively $\mathcal{R}^{*}$ and
${\mathcal{R}^{\theta}}^{*}$ are able to translate a local LTL property into a
global property without changing its semantics in terms of traces. Therefore,
we can use the two rewritings to prove Inference 2. Let
$\mathcal{M}_{1},\dots,\mathcal{M}_{n}$ be $n$ ITS and
$\varphi_{1},\dots,\varphi_{n}$ be LTL formulas on the language of each
$\mathcal{M}_{i}$. We define $\gamma_{P}$ as follows

$\gamma_{P}(\varphi_{1},\dots,\varphi_{n}):={\mathcal{R}^{\theta}}^{*}_{\mathcal{M}_{1}}(\varphi_{1})\wedge\dots\wedge{\mathcal{R}^{\theta}}^{*}_{\mathcal{M}_{n}}(\varphi_{n})\wedge\Psi_{cond}(\mathcal{M}_{1},\dots,\mathcal{M}_{n})$

######  Corollary 11.

Using $\gamma_{P}$ from Definition 5.10, $\gamma_{S}$ from Section 4.1, for
all compatible ITS $\mathcal{M}_{1},\dots,\mathcal{M}_{n}$, for all local
properties $\varphi_{1},\dots,\varphi_{n}$ over the language of respectively
$\mathcal{M}_{1},\dots,\mathcal{M}_{n}$, for all global properties $\varphi$:
Inference 2 holds.

######  Example 5.11.

Consider the formula $\varphi_{c2}:=G(rec_{2}\rightarrow
out_{2}^{\prime}=in_{2}\wedge Xsend_{2})$ from Figure 1. The rewriting
${{\mathcal{R}^{\theta}}}(\varphi_{c2})$ is defined as the following formula.

$G(\neg state\vee(\underbrace{run\wedge
rec_{2}}_{{{\mathcal{R}^{\theta}}}^{+}(rec_{2})}\rightarrow\underbrace{(end\vee\overbrace{out_{2}@\tilde{F}\neg
end}^{{\mathcal{R}^{\theta}}(out_{2}@\tilde{F}\top)}=in_{2})}_{{\mathcal{R}^{\theta}}(out_{2}^{\prime}=in_{2})}\wedge\underbrace{end\vee
Xsend_{2}}_{{{\mathcal{R}^{\theta}}}^{-}(Xsend_{2})}))$

Finally, ${{\mathcal{R}^{\theta}}}^{*}(\varphi_{c2})$ is defined as
${\mathcal{R}^{\theta}}(\varphi_{c2})$.

The simplification optimizes the formula in various parts. $Xsend_{2}$ is
rewritten into a simpler formula, in which we only need to check whether we
are at the end of the local trace; the same occurs for primed output variable
($next$). On the contrary, $G$ must be rewritten as for $\mathcal{R}$ because
its sub-formula is not stutter-tolerant. On the other hand, the top-level
rewriting is simplified because $G$ is syntactically stutter tolerant.

###  5.4. Rewriting under fairness assumption

This section defines a variation of the previous rewriting that assumes
infinite execution of local components. The rewriting is presented as a
variation of the optimized rewriting; it is meant to exploit the fairness
assumption to be more concise and efficient.

We define $\mathcal{R}^{\mathcal{F}}$ as follows:

$\displaystyle\mathcal{R}^{\mathcal{F}}(v):=v\text{ for }v\in V$
$\displaystyle\mathcal{R}^{\mathcal{F}}(Pred(u_{1},\dots,u_{n})):=Pred(\mathcal{R}^{\mathcal{F}}(u_{1}),\dots,\mathcal{R}^{\mathcal{F}}(u_{n}))$
$\displaystyle\mathcal{R}^{\mathcal{F}}(\varphi\vee\psi):=\mathcal{R}^{\mathcal{F}}(\varphi)\vee\mathcal{R}^{\mathcal{F}}(\psi)$
$\displaystyle\mathcal{R}^{\mathcal{F}}(\neg\varphi)=\neg\mathcal{R}^{\mathcal{F}}(\varphi)$
$\displaystyle\mathcal{R}^{\mathcal{F}}(X\psi):=\begin{cases}X(\mathcal{R}^{\mathcal{F}}(\psi))&\text{if
}\psi\text{ is synt. st.tol.}\\\ X(runR(\neg
run\vee\mathcal{R}^{\mathcal{F}}(\psi)))&\text{otherwise}\end{cases}$
$\displaystyle\mathcal{R}^{\mathcal{F}}(\varphi_{1}U\varphi_{2}):=\begin{cases}\mathcal{R}^{\mathcal{F}}(\varphi_{1})U\mathcal{R}^{\mathcal{F}}(\varphi_{2})&\text{if
}\varphi_{1}\text{ and }\varphi_{2}\text{ are synt. st.tol.}\\\ (\neg
run\vee\mathcal{R}^{\mathcal{F}}(\varphi_{1}))U(run\wedge\mathcal{R}^{\mathcal{F}}(\varphi_{2}))&\text{otherwise}\end{cases}$
$\displaystyle\mathcal{R}^{\mathcal{F}}(Y\varphi):=Y(\neg
runS(run\wedge\mathcal{R}^{\mathcal{F}}(\varphi)))$
$\displaystyle\mathcal{R}^{\mathcal{F}}(\varphi_{1}S\varphi_{2}):=\begin{cases}\mathcal{R}^{\mathcal{F}}(\varphi_{1})S\mathcal{R}^{\mathcal{F}}(\varphi_{2})&\text{if
}\varphi_{1}\text{ and }\varphi_{2}\text{ are synt. st.tol}\\\ (\neg
run\vee\mathcal{R}^{\mathcal{F}}(\varphi_{1}))S(run\wedge\mathcal{R}^{\mathcal{F}}(\varphi_{2}))&\text{otherwise}\end{cases}$
$\displaystyle\mathcal{R}^{\mathcal{F}}(ite(\psi,u_{1},u_{2})):=ite(\mathcal{R}^{\mathcal{F}}(\psi),\mathcal{R}^{\mathcal{F}}(u_{1}),\mathcal{R}^{\mathcal{F}}(u_{2}))$
$\displaystyle\mathcal{R}^{\mathcal{F}}(u@\tilde{F}\varphi):=\begin{cases}\mathcal{R}^{\mathcal{F}}(u)@\tilde{F}\mathcal{R}^{\mathcal{F}}(\varphi)&\text{if
}\psi\text{ is synt. st. tol.}\\\
\mathcal{R}^{\mathcal{F}}(u)@\tilde{F}(run\wedge\mathcal{R}^{\mathcal{F}}(\varphi))&\text{otherwise}\end{cases}$
$\displaystyle\mathcal{R}^{\mathcal{F}}(u@\tilde{P}\varphi):=\mathcal{R}^{\mathcal{F}}(u)@\tilde{P}(run\wedge\mathcal{R}^{\mathcal{F}}(\varphi))$

Moreover, we define ${\mathcal{R}^{\mathcal{F}}}^{*}$ as

${\mathcal{R}^{\mathcal{F}}}^{*}(\varphi):=\begin{cases}\mathcal{R}^{\mathcal{F}}(\varphi)&\text{
If }\varphi\text{ is synt. st. tol.}\\\ runR(\neg
run\vee\mathcal{R}^{\mathcal{F}}(\varphi))&\text{ Otherwise}\end{cases}$

${\mathcal{R}^{\mathcal{F}}}^{*}$ simplifies ${\mathcal{R}^{\theta}}^{*}$ in
various ways. It does not need to distinguish between input and output
variables, it does not distinguish between weak/strong semantics and it does
not distinguish between $state$ and $run$. Intuitively, these distinctions
make sense only with finite semantics; since the rewriting assumes infinite
local executions, these technicalities become superfluous.

######  Theorem 12.

Let $\pi$ be an infinite trace, for all $\pi^{ST}\in
Pr^{-1}(\pi):\pi\models\varphi\Leftrightarrow\pi^{ST}\models{\mathcal{R}^{\mathcal{F}}}^{*}(\varphi)$

######  Proof 5.12.

(Sketch) Since $\pi$ is infinite, $end$ is always false, $state\Leftrightarrow
run$. We can substitute $end$ with $\bot$ and $state$ with $run$ in
${\mathcal{R}^{\theta}}$ and we obtain this rewriting.

######  Example 5.13.

Consider the formula $\varphi_{c2}:=G(rec_{2}\rightarrow
out_{2}^{\prime}=in_{2}\wedge Xsend_{2})$ from Figure 1. The rewriting
${\mathcal{R}^{\mathcal{F}}}(\varphi_{c2})$ is defined as the following
formula.

$G(\neg
run\vee(\underbrace{rec_{2}}_{\mathcal{R}^{\mathcal{F}}(rec_{2})}\rightarrow\underbrace{(\overbrace{out_{2}^{\prime}}^{\mathcal{R}^{\mathcal{F}}(out_{2}^{\prime})}=in_{2})}_{\mathcal{R}^{\mathcal{F}}(out_{2}^{\prime}=in_{2})}\wedge\underbrace{Xsend_{2}}_{\mathcal{R}^{\mathcal{F}}(Xsend_{2})}))$

Finally, ${\mathcal{R}^{\mathcal{F}}}^{*}(\varphi_{c2})$ is defined as
$\mathcal{R}^{\mathcal{F}}(\varphi_{c2})$.

By assuming infinite executions of local traces it is possible to drastically
simplify the rewriting. Next outputs are left unchanged because they are
stutter tolerant and with infinite execution $end$ is not needed. Input
variables are also transparent to the rewriting because the infinite semantics
do not distinguish between input and output variables. As before, $G$ must be
rewritten because its sub-formula is not stutter-tolerant; however, in this
case, the rewriting can use $run$ instead of $state$ because the two
expressions are equivalent with infinite semantics. Finally, as before, the
top-level rewriting is simplified because $G$ is syntactically stutter
tolerant.

##  6\. Experimental evaluation

We implemented the compositional techniques proposed in this paper inside the
contract-based design tool OCRA[CDT13]. Our extension covers the contract
refinement check, in which a contract (defined as a couple $\langle
A,G\rangle$ of LTL formulae) is considered correct if its sub-component
contracts refine it. For simplicity, we consider contracts without assumptions
i.e. in which the assumption is $\top$; in this scenario, the refinement of
contracts is given by the compositional reasoning described in this paper. For
a detailed description of the assume-guarantee contract proof system employed
in the tool refer to [CT15b].

The objective of this experimental evaluation is to do both a quantitative and
a qualitative evaluation of our compositional approach differentiating
possibly finite and infinite semantics. Qualitatively, we compare the
verification results to assess how the finiteness impacts on the result,
observing also the required scheduling assumptions for possibly finite
systems. Quantitatively, we analyze the overhead of reasoning over a mix of
finite and infinite executions to analyse whether or not our rewriting scales
on real models. Due to the absence of equally expressible formalism to define
asynchronous composition, our comparison with related work is limited to
another rewriting suited only for local infinite systems with event-based
asynchronous composition[BBC+09].

Although we defined compositional reasoning with truncated semantics, in our
experiments we reason about global infinite executions and possibly finite
local executions. The experiments222The results of the experimental evaluation
can be found at https://es-
static.fbk.eu/people/bombardelli/papers/nfm22/expeval_journal.tar.gz were run
in parallel on a cluster with nodes with Intel Xeon CPU 6226R running at
2.9GHz with 32CPU, 12GB. The timeout for each run was two hours and the memory
cap was set to 2GB.

In this section, we denote the composition based on
${\mathcal{R}^{\theta}}^{*}$ as TrR(Truncated Rewriting); we denote the
composition based on ${\mathcal{R}^{\theta}}^{*}$ with additional constraints
to ensure infinite local executions as TrR+F (Truncated Rewriting + Fairness);
we denote the composition based on ${\mathcal{R}^{\mathcal{F}}}^{*}$ assuming
local infinite execution as TrRuFA (Truncated Rewriting under Fairness
Assumption).

(a) Comparison between TrR+F and TrRuFA over valid instances.

(b) Comparison between TrR and TrRuFA over valid instances.

(c) Comparison between TrR and TrRuFA over ”different” results.

(d) Comparison between TrR and TrRuFA over all the instances.

Figure 5. Scatter plots comparing TrR,TrR+F and TrRuFA Figure 6. Comparison
between TrRuFA and event-based rewriting of [BBC+09]

table.csv

Table 1. Subset of quantitative and qualitative results of the experimental
evaluation.

###  6.1. Benchmarks

We have considered benchmarks of various kinds:

  1. (1)

Simple asynchronous models from OCRA comprehending the example depicted in
Figure 1.

  2. (2)

Pattern formula compositions from [BT22] experimental evaluation

  3. (3)

Contracts from the experimental evaluation of [CCG+23] on AUTOSAR models
adapted for truncated semantics.

####  6.1.1. Simple asynchronous models

We considered two variations of the example model depicted in Figure 1: one
version considers all three components with both the possible outcome of
failure and success. The second version is composed only of components $c1$
and $c2$ and the global property states that eventually the message is sent.

The second model we are considering is a simple representation of a Wheel
Brake System with two Braking System Control Units (BSCU) connected to two
input braking pedals, a Selection Switch and an actual hydraulic component
that performs the actual brake. The top-level property states that if one of
the two pedals is pressed eventually the hydraulic component will brake.

####  6.1.2. Pattern models

We took from [BT22] some benchmarks based on Dwyer LTL patterns [DAC70]. The
considered LTL patterns are the following: response, precedence chain and
universality patterns. The models compose the pattern formulas in two ways: as
a sequence of $n$ components linked in a bus and as a set of components that
tries to write on the output port. These patterns are parametrised on the
number of components involved in the composition.

####  6.1.3. EVA AUTOSAR contracts

We took the experimental evaluation from the tool EVA[CCG+23] and we adapted
it for our compositional reasoning. The models are composed of various
components for which the scheduling is of two types: event-based and cyclic.
Event-based scheduling forces the execution of a component when some of its
input variables change while cyclic scheduling forces the execution of the
component every $n$ time units.

In addition to these models, we also considered a variation of a subset of
instances (described in Section 1.1.2) and we relaxed the scheduling
constraints allowing some components to become unresponsive at some point to
the original constraints. We forced an event-based scheduled component (Brake
Actuator) to be scheduled when its input changes but only until it ends;
moreover, we forced a cyclic scheduled component (Brake Watchdog) to run every
$n$ times units until it ends. Finally, assuming that one of the two
components runs infinitely often (i.e. does not become unresponsive), we check
if the composition still holds.

###  6.2. Experimental evaluation results

Figure 5 provide an overall comparison between TrR, TrR+F and TrRuFA in terms
of results and execution time. In these plots, the colour determines the
validity results: blue aggregates all the results without distinction between
valid and invalid; green considers valid instances of both techniques (if the
other algorithm returns valid, timeout is optimistically believed to be true);
yellow consider instances in which the two techniques had different results.

Overall, we checked 624 instances (208 for each rewriting); 406 of these
instances were proven valid, 88 were proven invalid and 60 instances timed
out. The general statistics can be found in Table 2

summary.csv

Table 2. Summary result for algorithms

Table 1 shows some relevant instances of the experimental evaluation
highlighting their execution time and their validity results.

##### Qualitative results

As we expected, there are differences in validity results between TrR and
TrRuFA. The pattern models cannot guarantee the validity of the composition
with the weak semantics without additional constraints over the composition.
Intuitively, it suffices that a single component is not scheduled to violate
bounded response properties.

Similarly, we compared the validity results of the 3 rewritings on a
simplified version of the example of Section 1.1.1; this variation of the
model contains only components $c_{1}$ and $c_{2}$. The simplified version was
proved valid using TrRuFA and TrR+F while a counterexample was found using
TrR. The simplified version is found invalid when $c_{1}$ is scheduled only a
finite amount of times failing to deliver the message to component $c_{2}$. On
the other hand, when we correct the model by adding the component $c_{3}$, the
composition is proved valid in all the 3 cases.

For what regards the EVA benchmarks, TrR and TrRuFA gave the same validity
results. That occurred because the scheduling constraints were quite strong;
in particular, the cyclic constraints implicitly forced components, such as
the watchdog, to run infinitely often. The event-based scheduled component
could have a finite execution but only if their input did not change from some
point on. Differently, updating the constraints by removing these implicit
infinite executions makes the property invalid using TrR. To fix these invalid
results, we updated the system assuming that at least one of the two
components runs infinitely often and we relaxed the global property increasing
the timed bound for the brake to occur from 2 time units to 3. Finally, the
corrected model was proved in all the 3 cases.

##### Quantitative results

Figure 5(a) shows the comparison between TrR+F and TrRuFA. In this case,
TrRuFA is more efficient than TrR+F. This is not surprising because the
generated formula assuming infinite local execution can be significantly
smaller than the general one. In general, we see that, regardless of the
result, TrRuFA can prove the property faster. We think that having to check
all the possible combinations of finite/infinite local execution provides a
significant overhead in the verification.

In figure 6, we compared TrRuFA with another rewriting for the composition of
temporal properties from [BBC+09]. The comparison has been done over a subset
of the pattern models. The number of instances in this evaluation is limited
because the rewriting of [BBC+09] supports only asynchronous composition with
synchronization events. It is clear from the figure that TrRuFA outperforms
this other rewriting.

##  7\. Conclusions

In this paper, we considered the problem of compositional reasoning for
asynchronous systems with LTL properties over input and output variables in
which local components are not assumed to run infinitely often. We introduced
a semantics based on the truncated semantics of Eisner and Fisman for LTL to
reason over finite executions of local components. We proposed a new rewriting
of LTL formulas that allows for checking compositional rules with temporal
satisfiability solvers. We then provided an optimized version of such
rewriting.

In the future, we will consider various directions for extending the framework
including real-time and hybrid specifications, optimizations based on the
scheduling of components and other communication mechanisms such as buffered
communication. Moreover, we will generalise our compositional reasoning for
assume/guarantee contracts based on [CT15b], for which we hypothesise that
assumptions must be treated with strong semantics.

## References

  * [BBC+09] Nikola Benes, Lubos Brim, Ivana Cerná, Jirí Sochor, Pavlína Vareková, and Barbora Buhnova.  Partial order reduction for state/event ltl.  In IFM, 2009.
  * [BCL+10] Lei Bu, Alessandro Cimatti, Xuandong Li, Sergio Mover, and Stefano Tonetta.  Model checking of hybrid systems using shallow synchronization.  In John Hatcliff and Elena Zucca, editors, Formal Techniques for Distributed Systems, pages 155–169, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg.
  * [BCTZ23] Alberto Bombardelli, Alessandro Cimatti, Stefano Tonetta, and Marco Zamboni.  Symbolic model checking of relative safety ltl properties.  In IFM 2023: 18th International Conference, IFM 2023, Leiden, The Netherlands, November 13-15, 2023, Proceedings, pages 302–320, Berlin, Heidelberg, 2023. Springer-Verlag.  doi:10.1007/978-3-031-47705-8_16.
  * [BK08] Christel Baier and Joost-Pieter Katoen.  Principles of Model Checking.  MIT Press, 2008.
  * [BSST09] Clark Barrett, Roberto Sebastiani, Sanjit A Seshia, and Cesare Tinelli.  Satisfiability Modulo Theories.  In Handbook of Satisfiability, pages 825–885. IOS Press, January 2009.  doi:10.3233/978-1-58603-929-5-825.
  * [BT22] Alberto Bombardelli and Stefano Tonetta.  Asynchronous Composition of Local Interface LTL Properties.  In NFM, pages 508–526, 2022.
  * [CCD+14] Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta.  The nuxmv symbolic model checker.  volume 8559, pages 334–342, 07 2014.  doi:10.1007/978-3-319-08867-9_22.
  * [CCG+23] Alessandro Cimatti, Luca Cristoforetti, Alberto Griggio, Stefano Tonetta, Sara Corfini, Marco Di Natale, and Florian Barrau.  Eva: a tool for the compositional verification of autosar models.  In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 3–10, Cham, 2023. Springer Nature Switzerland.
  * [CDT13] Alessandro Cimatti, Michele Dorigatti, and Stefano Tonetta.  Ocra: A tool for checking the refinement of temporal contracts.  pages 702–705, 11 2013.  doi:10.1109/ASE.2013.6693137.
  * [CGH94] Edmund M. Clarke, Orna Grumberg, and Kiyoharu Hamaguchi.  Another Look at LTL Model Checking.  Formal Methods in System Design, 10:47–71, 1994.
  * [CGM+19] Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, and Stefano Tonetta.  Smt-based satisfiability of first-order ltl with event freezing functions and metric operators.  Information and Computation, 272:104502, 12 2019.  doi:10.1016/j.ic.2019.104502.
  * [CMT11] Alessandro Cimatti, Sergio Mover, and Stefano Tonetta.  Hydi: A language for symbolic hybrid systems with discrete interaction.  pages 275–278, 08 2011.  doi:10.1109/SEAA.2011.49.
  * [CT15a] Alessandro Cimatti and Stefano Tonetta.  Contracts-refinement proof system for component-based embedded systems.  Science of Computer Programming, 97:333–348, 2015.  Object-Oriented Programming and Systems (OOPS 2010) Modeling and Analysis of Compositional Software (papers from EUROMICRO SEAA 12).  URL: https://www.sciencedirect.com/science/article/pii/S0167642314002901, doi:10.1016/j.scico.2014.06.011.
  * [CT15b] Alessandro Cimatti and Stefano Tonetta.  Contracts-refinement proof system for component-based embedded systems.  Science of Computer Programming, 97:333–348, 2015.  URL: https://www.sciencedirect.com/science/article/pii/S0167642314002901, doi:10.1016/j.scico.2014.06.011.
  * [DAC70] Matthew Dwyer, George Avrunin, and James Corbett.  Patterns in property specifications for finite-state verification.  Proceedings - International Conference on Software Engineering, 02 1970.  doi:10.1145/302405.302672.
  * [dAH01] Luca de Alfaro and Thomas A. Henzinger.  Interface automata.  In ESEC / SIGSOFT FSE, pages 109–120. ACM, 2001.
  * [DGV13] Giuseppe De Giacomo and Moshe Y. Vardi.  Linear Temporal Logic and Linear Dynamic Logic on Finite Traces.  In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI ’13. AAAI Press, 2013.
  * [EFH+03a] Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, and David Van Campenhout.  Reasoning with temporal logic on truncated paths.  In International Conference on Computer Aided Verification, 2003\.  URL: https://api.semanticscholar.org/CorpusID:9153840.
  * [EFH+03b] Cindy Eisner, Dana Fisman, John Havlicek, Anthony McIsaac, and David Van Campenhout.  The Definition of a Temporal Clock Operator.  In ICALP, volume 2719 of Lecture Notes in Computer Science, pages 857–870. Springer, 2003.
  * [FK18] Dana Fisman and Hillel Kugler.  Temporal Reasoning on Incomplete Paths: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part II, pages 28–52.  11 2018.  doi:10.1007/978-3-030-03421-4_3.
  * [JT96] B. Jonsson and Yih-Kuen Tsay.  Assumption/guarantee specifications in linear-time temporal logic.  Theor. Comput. Sci., 167:47–72, 1996.
  * [KV01] Orna Kupferman and Moshe Y Vardi.  Model checking of safety properties.  Formal Methods in System Design, 19(3):291–314, 2001.
  * [Lam94] Leslie Lamport.  Temporal logic of actions.  ACM Transactions on Programming Languages and Systems (TOPLAS), 16:872–923, 05 1994.  doi:10.1145/177492.177726.
  * [Lam97] Leslie Lamport.  The operators of tla.  06 1997.
  * [Lat03] Timo Latvala.  Efficient Model Checking of Safety Properties.  In SPIN, volume 2648 of Lecture Notes in Computer Science, pages 74–88. Springer, 2003.
  * [LBA+22] Cong Liu, Junaid Babar, Isaac Amundson, Karl Hoech, Darren D. Cofer, and Eric Mercer.  Assume-guarantee reasoning with scheduled components.  In NASA Formal Methods, 2022.  URL: https://api.semanticscholar.org/CorpusID:248991390.
  * [LPZ85] O. Lichtenstein, A. Pnueli, and L.D. Zuck.  The Glory of the Past.  In Logics of Programs, pages 196–218, 1985.
  * [McM99] Kenneth L. McMillan.  Circular Compositional Reasoning about Liveness.  In CHARME, volume 1703 of Lecture Notes in Computer Science, pages 342–345. Springer, 1999.
  * [MP92a] Z. Manna and A. Pnueli.  The temporal logic of reactive and concurrent systems - specification.  Springer, 1992.
  * [MP92b] Zohar Manna and Amir Pnueli.  The temporal logic of reactive and concurrent systems - specification.  Springer, 1992.
  * [PDH99] Corina S. Pasareanu, Matthew B. Dwyer, and Michael Huth.  Assume-Guarantee Model Checking of Software: A Comparative Case Study.  In SPIN, volume 1680 of Lecture Notes in Computer Science, pages 168–183. Springer, 1999.
  * [Pnu77] Amir Pnueli.  The temporal logic of programs.  pages 46–57, 09 1977.  doi:10.1109/SFCS.1977.32.
  * [RBH+01] Willem-Paul Roever, Frank Boer, Ulrich Hannemann, Jozef Hooman, Yassine Lakhnech, Mannes Poel, and Job Zwiers.  Concurrency Verification: Introduction to Compositional and Noncompositional Methods.  01 2001.
  * [Roz11] Kristin Y. Rozier.  Linear temporal logic symbolic model checking.  Computer Science Review, 5(2):163–203, 2011.  URL: https://www.sciencedirect.com/science/article/pii/S1574013710000407, doi:10.1016/j.cosrev.2010.06.002.
  * [RR09] Ondrej Rysavy and Jaroslav Rab.  A formal model of composing components: The tla+ approach.  Innovations in Systems and Software Engineering, 5:139–148, 06 2009\.  doi:10.1007/s11334-009-0089-0.
  * [Ton17] Stefano Tonetta.  Linear-time Temporal Logic with Event Freezing Functions.  In GandALF, volume 256 of EPTCS, pages 195–209, 2017.