11institutetext: Department of Mathematics and Statistics,
University of Helsinki,
Helsinki,
Finland
11email: {juha.kontinen, max.sandstrom}@helsinki.fi22institutetext: Department of Computer Science,
University of Sheffield,
Sheffield,
UK
22email: [email protected]
A Remark on the Expressivity of Asynchronous
TeamLTL and HyperLTL
Linear temporal logic (LTL) is used in system verification
to write formal specifications for reactive systems.
However, some relevant properties,
e.g. non-inference in information flow security,
cannot be expressed in LTL.
A class of such properties that has recently
received ample attention
is known as hyperproperties.
There are two major streams in the research regarding
capturing hyperproperties, namely
hyperlogics, which extend LTL with trace quantifiers (HyperLTL),
and logics that employ team semantics,
extending truth to sets of traces.
In this article we explore the relation between asynchronous
LTL under set-based
team semantics (TeamLTL) and HyperLTL.
In particular we consider the extensions of TeamLTL with
the Boolean disjunction and a fragment of the extension of
TeamLTL with the Boolean negation, where the negation
cannot occur in the left-hand side of the Until-operator or
within the Global-operator.
We show that TeamLTL extended with
the Boolean disjunction is equi-expressive with
the positive Boolean closure of HyperLTL restricted to
one universal quantifier,
while the left-downward closed fragment of
TeamLTL extended with the Boolean negation
is expressively equivalent with
the Boolean closure of HyperLTL restricted to
one universal quantifier.
Keywords:
Hyperproperties Temporal Logic Team Semantics HyperLTL Verification
1 Introduction
In 1977 Amir Pnueli [15] introduced
a core concept in verification of reactive and
concurrent systems: model checking of formulae of
linear temporal logic ().
The idea is to view the accepting executions of
the system as a set of infinite sequences, called traces,
and check whether this set satisfies specifications
expressed in .
The properties that can be checked by observing
every execution of the system in isolation are called
trace properties.
An oft-cited example of a trace property is termination,
which states that a system terminates if each of its computations
terminates.
Classical is fit for
the verification of such propositional trace properties,
however some properties relevant in, for instance,
information flow security are not trace properties.
These properties profoundly speak of relations between traces.
Clarkson and Schneider [3] coined the term
hyperproperties to refer to such properties
that lie beyond what can express.
Bounded termination is an easy to grasp example of
a hyperproperty:
whether every computation of
a system terminates within some bound common for all traces,
cannot be determined by looking at traces in isolation.
In information flow security, dependencies between
public observable outputs and
secret inputs constitute possible security breaches;
checking for hyperproperties
becomes invaluable.
Two well-known examples of hyperproperties from this field are
noninterference
[17, 14],
where a high-level user cannot affect
what low-level users see,
and observational determinism [20],
meaning that if two computations are in the same state
according to a low-level observer,
then the executions will be indistinguishable.
However, hyperproperties are not
limited to information flow security;
examples from different fields
include distributivity and
other system properties such as
fault tolerance [6].
Given this background, several approaches to
formally specifying hyperproperties
have been proposed since 2010,
with families of logics emerging from these approaches.
The two major streams in the research regarding
capturing hyperproperties are
hyperlogics and logics that employ team semantics.
In the hyperlogics approach,
logics that capture trace properties
are extended with trace quantification,
extending logics such as , computation tree logic () or
quantified propositional temporal logic (),
into [2],
[2],
and [16, 4],
respectively.
An alternative approach is to lift the semantics
of the temporal logics from being
defined on traces to sets of traces,
by using what is known as team semantics.
This approach yields logics such as
[13, 8] and
[12, 8].
Since its conception, has been considered in
two distinct variants:
a synchronous semantics,
where the team of traces agrees on the time step
of occurrence when evaluating temporal operators;
and an asynchronous semantics,
where the temporal operators are evaluated
independently on each trace.
An example that illustrates the difference between
these two semantics is
the aforementioned termination and
bound termination pair of properties.
If we write for the future-operator and
for
a proposition symbol representing the trace terminating,
we can write the formula ,
which under the synchronous semantics expresses the hyperproperty
“bounded termination”,
while under the asynchronous semantics
the same formula defines the trace property
“termination”.
Not only is the above formulation of
bounded termination clear and concise,
it also illuminates a key difference between
hyperlogics and team logics:
while each formula of hyperlogic has
a fixed number of quantifiers,
which restricts the number of traces that can be referred to
in a formula, which restricts the number of traces
between which dependencies can be characterised by formulae,
team logics have the ability to refer to
an unbounded number of traces, even an infinite collection.
One of the original motivations behind
team semantics [18]
was to enable the definition of novel atomic formulae,
and this is another important defining feature of
team temporal logics
as well.
Among these atoms the dependence atom
and
inclusion atom
stand out as the most influential.
They respectively state that
the variables are
functionally dependent on
the variables ,
and that the values of
the variables
also occur among the values of variables .
As an example of the use of the inclusion atom,
let the proposition symbols
denote public observable bits and
assume that the proposition symbol
is a secret bit.
The atomic formula
expresses a form of non-inference by stating that an observer
cannot infer the value of the confidential bit from the outputs.
While the expressivity of and
other hyperlogics has been studied extensively,
where the many extensions of lie in relation the hyperlogics is still not
completely understood.
The connections for the logics without extensions were already
established in Krebs et al. [13],
where they showed that synchronous and
are expressively incomparable and that
the asynchronous variant collapses to .
With regards to the expressivity of synchronous semantics,
Virtema et al. [19]
showed that the extensions of can be translated to ,
which in turn extends with (non-uniform)
quantification of propositions.
Relating the logics to the first-order context,
Kontinen and Sandström [10] defined
Kamp-style translations from
extensions of both semantics of to
the three-variable fragment of first-order team logic.
It is worth noting that recently asynchronous hyperlogics
have been considered also in several other articles
(see, e.g., [9, 1]).
An example of the significant rift between
asynchronous and synchronous
is that the asynchronous semantics is essentially
a first-order logic,
while the synchronous semantics has
second-order aspects.
Especially the set-based variant of asynchronous
can be translated, using techniques in [10],
into first-order logic under team semantics,
which is known to be first-order logic [18].
Similarly, is equally expressive as
the guarded fragment of
first-order logic with the equal level predicate,
as was shown by Finkbeiner and Zimmermann [7].
In this article we focus on exploring
the connections between fragments of and
extensions of .
The set-based asynchronous semantics that we consider here
was defined in Kontinen et al. [11] in order to
further study the complexity of
the model checking problem for these logics.
Prior to that, the literature on temporal team semantics
employed a semantics based on multisets of traces.
In the wider team semantics literature,
this often carries the name strict semantics,
in contrast to lax semantics which is de facto a
set-based semantics.
This relaxation of the semantics enabled
the definition of normal forms for the logics,
which we use in this article to explore the connection
with .
Our contribution.
We show correspondences in expressivity between
the set-based variant of
linear temporal logic under asynchronous team semantics and
fragments of the Boolean closure of .
In particular we show that under
team semantics with the Boolean disjunction,
, is equi-expressive with
the positive Boolean closure of restricted to
only one universal quantifier,
while the left downward closed fragment of
is equi-expressive with
the Boolean closure of restricted to
one universal quantifier.
2 Preliminaries
We begin by defining
the variant of and
its extensions,
as in [11].
Let be a set of atomic propositions.
The formulae of (over ) is attained by
the grammar:
where .
We follow the convention that
all formulae of are given in
negation normal form,
where is only allowed before atomic propositions,
as is customary when dealing with team semantics.
We will consider the extensions of with
the Boolean disjunction , denoted ,
and Boolean negation , denoted .
A trace over is an
infinite sequence of sets of proposition symbols from
.
Given a natural number , we denote by
the th element of and by
the suffix of .
We call a set of traces a team.
We write
to denote
.
For a team a function
,
we set
.
For , ,
and ,
we define that if and only if
Definition 1 ()
Let be a team, and and
-formulae.
The lax semantics is defined as follows.
The semantics for the Boolean disjunction and Boolean negation,
used in the extensions and ,
are given by:
Note that the Boolean disjunction is
definable in ,
as the dual of conjunction,
i.e.
if and only if
.
Two important properties of team logics are
flatness and downward closure.
A logic has the flatness property if
if and only if
for all ,
holds for all formulae of the logic.
A logic is downward closed if for
all formulae of the logic
if and
then .
The following Proposition was proven in [11].
Proposition 1
has both the flatness and
the downward closure properties, while
only has the downward
closure property.
We consider the left-downward closed fragment of
, denoted ,
where every subformula of the form or ,
the subformula is a -formula
It was established in [11] that any formula of
can be equivalently expressed in
-disjunctive normal form, i.e. in the form
where are -formulae.
Similarly by [11],
every formula of
can be equivalently stated in quasi-flat normal form,
which means in the form
where and are -formulae,
and is an abbreviation for
the formula ,
where is
the formula obtained from ,
after has been pushed down to the atomic level.
Next we state the syntax and semantics of ,
as defined in [2],
as well as the Boolean closure concepts we are concerned with.
Definition 2 (Syntax of )
Let be a set of propositional variables and
the set of all trace variables.
Formulas of are generated by the following grammar:
where and .
We denote the set of all traces by and
the set of all trace variables by .
For a trace assignment function
,
we write for
the trace assignment defined through
,
and for the assignment that
assigns to ,
but otherwise is identical to .
Definition 3 (Semantics of )
Let be a proposition symbol,
be a trace variable,
be a set of traces, and
let be
a trace assignment.
Definition 4 (Universal Fragments)
The universal fragment of ,
denoted by ,
is the fragment of with
no existential quantification.
We write for
the one variable universal fragment of ,
and for the one variable fragment of .
Definition 5 ((Positive) Boolean Closure)
The Boolean closure of a logic ,
denoted by , is
the extension of that is
closed under , and .
The positive Boolean closure of
a logic ,
denoted by , is
the extension of that is closed under
and .
The semantics for the Boolean closures are attained by relaxing
the definition of conjunction ,
disjunction , and to
apply to any formula of the Boolean closure.
Using a suitable algorithm,
all -formulae can be
equivalently expressed in disjunctive normal form,
i.e. as a disjunction of conjunctions
with possibly a negation in
front of each formula of .
Similarly, all -formulae
can be equivalently expressed as
for some formulae and
index sets and .
From here on we use and to denote arbitrary index sets.
3 Correspondence between and
In this section we will explore
the relationship between the logics by
proving some correspondence theorems.
First, however, we prove some pertinent propositions regarding
the Boolean closure of ,
showing that conjunction, disjunction and
negation distribute over
the quantifiers in a manner analogous to first-order logic.
We go through these propositions in some detail as,
although they appear familiar from the first-order setting,
is usually considered only in the prenex normal form
and thus these basic results are not explicitly addressed in
the literature.
Moreover, the proofs feature arguments that
will be useful in subsequent proofs.
As usual, for logics and ,
we write ,
if for every -formula
there exists an equivalent -formula.
We write ,
if both and
.
Proposition 2
Proof
Let
be an arbitrary formula of
.
If all are quantifier free,
we are done, as then
is a
-formula.
Thus, we may assume that
for some -formula .
Suppose
Without loss of generality,
we may assume a uniform quantifier block in each conjunct,
as one can rename variables and take the largest quantifier
block as the common one,
since redundant quantifiers do not effect evaluation.
The previous is therefore equivalent with
At this point,
we wish to push the disjunction past the quantifier block,
but the variables would become entangled and
different traces could satisfy different disjuncts.
We need to distinguish the variables of
the disjuncts from each other,
so we rename the trace quantifiers.
The previous evaluation is therefore equivalent with
This is a formula of . ∎
The following remark, familiar from first-order logics,
can be proven with a straight-forward induction over
the length of the quantifier block.
Remark 1
For -formula it holds that
where for every index ,
are quantifiers or ,
and is if is
and vice versa.
Proposition 3
Proof
Consider a -formula
in
disjunctive normal form,
with either or
for some formula .
By Remark 1 ,
where .
Thus we may assume that
only appears positively.
By a similar argument to that of the proof of Proposition
2 we get the following:
∎
One last remark before we get to
the core results of this article,
this time relating quantifier-free -formulae with
-formulae.
The remark can again be proven by induction on
the structure of the formula.
Remark 2
Let be a team, be a trace assignment,
be a trace variable,
be a -formula,
and let be
the formula identical to ,
except every proposition symbol is replaced by .
Suppose for some .
Now the following equivalence holds
Using the above propositions we may now proceed with proving
our main results:
correspondence theorems between team logics and
the Boolean closures of hyperlogics.
Note that has no separation between
closed and open formulae,
and has no features to encode trace assignments.
Thus, when is a formula of some
team based logic and
is a formula of a hyper logic
without free variables,
we say that and are equivalent,
if the equivalence
,
holds for all sets of traces .
The notations and
are then defined in the obvious way,
by restricting to
formulae without free variables.
Theorem 3.1
Proof
Let be an arbitrary team and
an arbitrary -formula.
By [11, Theorem 10],
we may assume that is in
the form ,
where in an index set and
are -formulae.
We let denote
the -formulae obtained from ,
by replacing every proposition symbol by
.
We obtain the following chain of equivalences:
where
the first equivalence follows from the semantics of ,
the second equivalence holds by the flatness of ,
the third equivalence is due to
the semantics of and
Remark 2,
and the final equivalence follows from
the semantics of .
For the converse direction, consider an arbitrary
-sentence .
As noted above, is equivalent to a sentence
,
where , for every pair and ,
is a -formula with as the only free variable.
Now by an argument similar to the proof of
Proposition 2,
if and only if
.
Equivalently then by the definition of the semantics of
the disjunction,
we may fix such that
.
By the definition of the universal quantifier then
we get that
the previous is equivalent with
for all .
Now by Remark 2,
the previous holds if and only if
,
which is equivalent to
,
due to the flatness property of .
Finally, by the semantics of the Boolean disjunction,
the previous is equivalent with
. ∎
As a corollary we get that is subsumed by
the universal fragment of ,
which follows from Theorem 3.1 and
the observations made in the proof of
Proposition 2.
Corollary 1
Note that another consequence of
Theorem 3.1
is that is strictly
less expressive than ,
as the former is equivalent with [5]
and thus has the flatness property,
while the latter is equivalent with ,
which does not satisfy flatness.
This stands in contrast to the unrestricted
universal fragment ,
which by Proposition 2
is equivalent to its positive Boolean closure.
Theorem 3.2
Proof
Let be an arbitrary
-formula.
Now by the quasi-flat normal form
if and only if
.
Equivalently, by the semantics of ,
we may fix an index such that
.
By the semantics of the logic,
flatness, and the interpretation of the shorthand ,
the previous evaluation is equivalent with that
for all and
for all there is a such that
.
By Remark 2 the previous holds
if and only if
for all
and for all there is a such that
.
Equivalently, by the semantics of and ,
we have that
and
,
which, finally by the semantics of and ,
holds if and only if
.
On the other hand,
let be an arbitrary sentence of .
Now we get the following chain of equivalences,
where :
where the first equivalence is due to
the normal form for a Boolean closure,
the second equivalence is holds because
the universally quantified conjuncts can
equivalently be evaluated simultaneously,
the third equivalence follows from
the semantics of and ,
the fourth equivalence holds by
the semantics of and ,
the fifth equivalence holds by
Remark 2,
the sixth equivalences is due to flatness and
the definition of the shorthand ,
the seventh equivalence holds by
the semantics of ,
and the final equivalence follows from
the semantics of .
The other equivalence in the theorem is a
direct consequence of
Remark 1.∎
4 Conclusion
In this article we explored
the connections in expressivity between
extensions of linear temporal logic under
set-based team semantics ()
and fragments of linear temporal logic
extended with trace quantifiers ().
We showed that ,
when extended with the Boolean disjunction,
corresponds to the positive Boolean closure of
the one variable universal fragment of .
Furthermore we considered
a fragment of extended with the Boolean negation,
where the formulae are restricted to
not to contain the Boolean negation
on the left-hand side of the ‘until’ operator () or
under the ‘always going to’ () operator.
We showed a correspondence between that fragment and
the Boolean closure of
the one variable universal fragment of .
From our results it follows that
the logics considered are all
true extensions of .
Decidability of the model checking and satisfaction problems
for the team based logics was shown in [11],
and by our correspondence results
(and the translation implied by the proofs of the theorems),
decidability of the problems
extends to the hyperlogics in question as well.
It is fascinating to see that the restriction to
left downward closed formulae in
the latter correspondence on the team logic side
disappears on the hyperlogic side.
This hints at that the fragment considered is intuitive.
It is an open question whether the downward closed
fragment of is ,
or if some restricted use of the Boolean negation
could be allowed and still maintain downward closure.
Another open question is whether
an analogous correspondence exists for
the full logic ,
or even for some lesser restriction of the logic
than the left-downward closed fragment.
{credits}
Acknowledgements.
This work was supported by
the Academy of Finland grant 345634 and
the DFG grant VI 1045/1-1.
References
[1]
Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez.
A temporal logic for asynchronous hyperproperties.
In CAV (1), volume 12759 of Lecture Notes in Computer Science, pages 694–717. Springer, 2021.
[2]
Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez.
Temporal logics for hyperproperties.
In POST 2014, pages 265–284, 2014.
[3]
Michael R. Clarkson and Fred B. Schneider.
Hyperproperties.
Journal of Computer Security, 18(6):1157–1210, 2010.
[4]
Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann.
The hierarchy of hyperlogics.
In LICS 2019, pages 1–13. IEEE, 2019.
[6]
Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup.
Synthesis from hyperproperties.
Acta Informatica, 57(1-2):137–163, 2020.
doi:10.1007/s00236-019-00358-2.
[7]
Bernd Finkbeiner and Martin Zimmermann.
The first-order logic of hyperproperties.
In Heribert Vollmer and Brigitte Vallée, editors, STACS 2017, volume 66 of LIPIcs, pages 30:1–30:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
[8]
Jens Oliver Gutsfeld, Arne Meier, Christoph Ohrem, and Jonni Virtema.
Temporal team semantics revisited.
In Christel Baier and Dana Fisman, editors, LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 44:1–44:13. ACM, 2022.
doi:10.1145/3531130.3533360.
[9]
Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem.
Automata and fixpoints for asynchronous hyperproperties.
Proc. ACM Program. Lang., 5(POPL):1–29, 2021.
doi:10.1145/3434319.
[10]
Juha Kontinen and Max Sandström.
On the expressive power of teamltl and first-order team logic over hyperproperties.
In WoLLIC, volume 13038 of Lecture Notes in Computer Science, pages 302–318. Springer, 2021.
[11]
Juha Kontinen, Max Sandström, and Jonni Virtema.
Set semantics for asynchronous teamltl: Expressivity and complexity.
In Jérôme Leroux, Sylvain Lombardy, and David Peleg, editors, 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023, August 28 to September 1, 2023, Bordeaux, France, volume 272 of LIPIcs, pages 60:1–60:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
URL: https://doi.org/10.4230/LIPIcs.MFCS.2023.60, doi:10.4230/LIPICS.MFCS.2023.60.
[12]
Andreas Krebs, Arne Meier, and Jonni Virtema.
A team based variant of CTL.
In Fabio Grandi, Martin Lange, and Alessio Lomuscio, editors, 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015, Kassel, Germany, September 23-25, 2015, pages 140–149. IEEE Computer Society, 2015.
doi:10.1109/TIME.2015.11.
[13]
Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann.
Team Semantics for the Specification and Verification of Hyperproperties.
In Igor Potapov, Paul Spirakis, and James Worrell, editors, MFCS 2018, volume 117, pages 10:1–10:16, Dagstuhl, Germany, 2018. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
[14]
John McLean.
Proving noninterference and functional correctness using traces.
Journal of Computer Security, 1(1):37–58, 1992.
doi:10.3233/JCS-1992-1103.
[15]
Amir Pnueli.
The temporal logic of programs.
In 18th Annual Symposium on Foundations of Computer Science, pages 46–57. IEEE Computer Society, 1977.
[16]
Markus N. Rabe.
A Temporal Logic Approach to Information-Flow Control.
PhD thesis, Saarland University, 2016.
[17]
A. W. Roscoe.
CSP and determinism in security modelling.
In Proceedings of the 1995 IEEE Symposium on Security and Privacy, Oakland, California, USA, May 8-10, 1995, pages 114–127. IEEE Computer Society, 1995.
doi:10.1109/SECPRI.1995.398927.
[18]
Jouko Väänänen.
Dependence Logic.
Cambridge University Press, 2007.
[19]
Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang.
Linear-time temporal logic with team semantics: Expressivity and complexity.
In Mikolaj Bojanczyk and Chandra Chekuri, editors, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021, December 15-17, 2021, Virtual Conference, volume 213 of LIPIcs, pages 52:1–52:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
doi:10.4230/LIPIcs.FSTTCS.2021.52.
[20]
Steve Zdancewic and Andrew C. Myers.
Observational determinism for concurrent program security.
In 16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), 30 June - 2 July 2003, Pacific Grove, CA, USA, page 29. IEEE Computer Society, 2003.
doi:10.1109/CSFW.2003.1212703.