PaperlayerView exact revision on arXiv

Source-linked AI summary

A Theory of Sampling for Continuous-time Metric Temporal Logic

Carlo A. Furia, Matteo Rossi

arXiv:0911.5642v2cs.LO

TL;DR

The paper asks how MTL semantics over continuous time relate to semantics over discrete time obtained by sampling, a question arising in modeling and analyzing systems with continuous and discrete components. It develops conditions and transformations relating the two, proving sampling invariance for flat MTL and using the relation for a verification technique that remains incomplete.

  • Problem

    The paper studies when sampled discrete-time behaviors capture continuous-time MTL semantics for systems combining continuous and discrete components.

    Source: §1 · p. 3, §3.1.2 · p. 12

  • Method

    The paper relates continuous-time MTL formulas to transformed discrete-time counterparts under sampling, with sampling-invariance results for flat MTL.

    Source: §3.3.2 · p. 18, §3.4 · p. 24

  • Results

    All flat MTL formulas are sampling invariant under the canonical adaptations, and the resulting discretization-based verification technique is inherently incomplete.

    Source: §3.3.2 · p. 18, §6 · p. 37

  • Takeaways & Limitations

    The relation supports reducing verification of dense-time MTL system descriptions to discrete time, where the paper reports practical efficiency in related implementations.

    Source: §1 · p. 4, §4.3 · p. 32

    The verification technique is inherently incomplete, and finding a model form whose approximations avoid incompleteness can require non-trivial effort.

    Source: §4.3 · p. 32, §6 · p. 37

Abstract

from arXiv · show

This paper revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiability of Metric Temporal Logic (MTL) formulas over continuous-time models and over discrete-time models is studied. It is shown to what extent discrete-time sequences obtained by sampling continuous-time signals capture the semantics of MTL formulas over the two time domains. The main results apply to "flat" formulas that do not nest temporal operators and can be applied to the problem of reducing the verification problem for MTL over continuous-time models to the same problem over discrete-time, resulting in an automated partial practically-efficient discretization technique.

1 Introduction

The paper adapts sampling to MTL analysis of systems combining continuous and discrete components. It relates continuous-time formulas to discrete-time counterparts and uses that relation for a partial verification reduction.

1 Introduction

  • The paper addresses the challenge of modeling and analyzing systems that combine continuous signals with discrete computer programs [FMMR10].This is framed as a central challenge in research on real-time and hybrid systems.Source: §1 · p. 3
  • Sampling converts continuous-time signals into discrete-time counterparts that serve as an interface, retaining partial information for discrete components.The approach transfers this engineering idea to formal modeling and analysis with real-time temporal logic.Source: §1 · p. 3
  • MTL formulas model component behaviors over either continuous or discrete time, with syntactic transformations accounting for information preserved when moving between interpretations.A continuous-time formula's transformed discrete-time counterpart is satisfied by discrete behaviors obtained by sampling its continuous-time behaviors.Source: §1 · p. 3
  • The sampled continuous-time behaviors must be non-Berkeley—sufficiently slow relative to the sampling process—for information preservation.This is an additional requirement on sampled behaviors.Source: §1 · p. 4
  • Sampling invariance relates continuous-time MTL formulas to suitable discrete-time counterparts, supporting an automated but partial reduction of verification to the discrete-time case.The paper focuses on the mathematical relationship between the two semantics, not implementation or practical performance.Source: §1 · p. 4

2 Metric Temporal Logic(s)

This section establishes the behavior models, MTL syntax, and semantics used to study dense- and discrete-time formulas. It focuses on flat MTL, whose formulas do not nest temporal operators.

2 Metric Temporal Logic(s)

  • MTL formulas combine propositional formulas with bounded temporal modalities, and the paper studies how their models and satisfiability vary across time domains.The section uses R and Z for real and integer time, respectively, and defines intervals as convex subsets of a time domain.Source: §2 · p. 4, §2.2.1 · p. 6

2.1 Behaviors

  • Behaviors map each time instant to the propositions holding then; non-Zeno behaviors admit a countable partition into adjacent intervals on which the behavior is constant.Non-Berkeleyness further requires each maximal constancy interval to contain a closed interval of size δ.Source: §2.1 · pp. 5–6

2.2 MTL: Syntax and Semantics

  • MTL syntax combines propositional formulas using Boolean connectives and bounded until, since, release, and trigger modalities.Intervals may be unbounded and may have negative endpoints; the syntax assumes negation normal form.Source: §2.2.1 · p. 6

2.2.1 MTL Syntax

  • Flat MTL restricts temporal modalities to propositional arguments, so its formulas do not nest temporal operators.LTL is the subset in which all intervals are [0, +∞).Source: §2.2.1 · pp. 6–7

2.2.2 MTL Semantics

  • MTL semantics evaluates formulas over behaviors and time instants; the paper's global satisfiability convention requires a formula to hold at every instant.The semantics defines temporal modalities through conditions on future or past instants within their intervals.Source: §2.2.2 · pp. 7–8

2.2.3 Derived Operators and Variants

  • Derived operators include quantitative eventually and globally, all-time and sometime operators, dense-time nowon variants, and matching variants of until and release.Non-Berkeley behaviors also yield a δ-separated constancy property for propositional formulas.Source: §2.2.3 · p. 8

2.3 Relations with Other Metric Temporal Logics

The section compares MTL fragments and satisfiability semantics, showing how flat formulas can represent globally satisfiable formulas while remaining less expressive. It also discusses the consequences of non-Berkeleyness for flattening and contrasts dense- and discrete-time decidability.

2.3.1 Expressiveness

  • Global satisfiability for flat MTL is more expressive than initial satisfiability, allowing common bounded-response and bounded-invariance properties to be expressed.This motivates the paper’s use of global satisfiability for results focused on the flat fragment.Source: §2.3.1 · p. 9
  • Flat MTL is strictly less expressive than full MTL, yet every MTL formula can be flattened into a globally equisatisfiable flat formula using auxiliary propositions.For dense-time non-Berkeley behaviors, flattening is more intricate and can break non-Berkeleyness; the example shows the resulting formulas need not be equi-satisfiable for any δ > 0.Source: §2.3.1 · p. 10
  • Strict until is more expressive than non-strict until for flat MTL, although all until variants have the same expressive power over dense- and discrete-time behaviors.The paper adopts non-strict non-matching until because it makes the presentation of results more natural.Source: §2.3.1 · p. 11

2.3.2 Decidability and Complexity

  • Full MTL and flat MTL are undecidable over non-Zeno dense-time behaviors, while discrete-time MTL and MTL over non-Berkeley dense-time behaviors are decidable with EXPSPACE-complete complexity.The flat-fragment satisfiability problem is inter-reducible with that of full MTL.Source: §2.3.2 · p. 11

3 Sampling Invariance

The section uses the reals as dense continuous time and the integers as discrete time, while noting that nearly all definitions and results can be adapted to other dense/discrete domain pairs.

3 Sampling Invariance

  • Nearly all definitions and results can be adapted with little effort from the reals and integers to other dense/discrete time-domain pairs, including nonnegative reals and naturals.The section assumes R as dense continuous time and Z as discrete time.Source: §3 · p. 11

3.1 Definitions

The section defines sampling as a map from dense-time behaviors to discrete-time behaviors and investigates when sampling preserves MTL semantics. It accounts for differences in time units, granularity, and behavior-change speed through adaptations and non-Berkeleyness.

3.1.1 Sampling Functions

  • A sampling function maps dense-time behaviors to discrete-time behaviors; canonical sampling observes a behavior at integer multiples of period δ from origin z.The canonical sampling map is onto and total for any δ and z.Source: §3.1.1 · p. 11

3.1.2 On Dense- vs. Discrete-Time Semantics

  • Dense/discrete semantics differ in units and granularity, so formula intervals are scaled and rounded conservatively; behavior changes faster than sampling can also hide truth values.The section introduces non-Berkeleyness to constrain behavior speed and adaptation functions to modify intervals for the time-domain change.Source: §3.1.2 · pp. 12–13

3.1.3 Sampling Invariance

  • Sampling invariance relates formula models across time domains using sampling functions, a sampling period, and adaptations, with closure under sampling or inverse sampling defined for the relevant endpoint type.The section seeks conditions under which discrete-time models are precisely the samplings of continuous-time models.Source: §3.1.2 · p. 12, §3.1.3 · p. 13

3.2 Illustrative Examples

The examples motivate requiring non-Berkeley behaviors at the sampling period and illustrate how formula types affect preservation between dense and discrete time. Inverse sampling is more difficult, particularly for existential formulas and until.

3.2 Illustrative Examples

  • Non-Berkeleyness must use the sampling period: otherwise a dense-time formula can hold everywhere while its proposition is false at every sampled instant.The example uses 3[2,5](p) and a behavior whose truth-value changes too quickly relative to sampling.Source: §3.2 · p. 15
  • Under non-Berkeleyness, existential and universal formulas can be sampled without changing their intervals beyond scaling time units.For existential formulas, a truth interval reaches a sampling instant; the example for universal formulas preserves the same endpoints.Source: §3.2 · p. 15
  • Inverse sampling requires expanding existential intervals and shrinking universal intervals to account for uncertainty of up to one sampling period on each side.The examples adapt [2,5] to [1,6] for an existential formula and [2,5] to [3,4] for a universal formula.Source: §3.2 · pp. 15–16
  • Until is closed under sampling in the example, but inverse sampling may require weakening its second argument or using a matching-until variant.A sampled behavior can arise from a dense-time behavior where the non-matching until formula fails.Source: §3.2 · p. 16

3.3 Sampling Invariance for MTL

This section examines how interval adaptations affect sampling and satisfiability for flat MTL formulas, including canonical adaptations that make sampling invariant and a regular adaptation that does not preserve continuous-time satisfiability. It also states a satisfiability result for discrete-endpoint formulas using U↓, S↓, R, and T.

3.3.1 Canonical Adaptations

  • The until and since adaptations are asymmetric to reconcile non-matching discrete- and dense-time semantics; matching variants preserve symmetry.The treatment also includes matching discrete-endpoint operators, which are used in Section 4.Source: §3.3.1 · p. 17

3.3.2 Flat MTL is Sampling Invariant

  • For any sampling period δ > 0 and origin z, all flat MTL formulas are sampling invariant under the canonical adaptations.The proof establishes closure under sampling for dense-endpoint formulas and closure under inverse sampling for discrete-endpoint formulas.Source: §3.3.2 · p. 18

3.3.3 Canonical Adaptations are Optimal

  • Canonical adaptations are the most constraining among regular sampling-invariant adaptations, and preserve formula structure except for interval adjustments.The paper defines regularity through compositionality, propositional preservation, and modality preservation; a regular adaptation preserving the non-matching until modality would not achieve sampling invariance.Source: §3.3.3 · p. 22
  • A constructed formula ζ = x ∨ ϕ is continuously satisfiable but fails sampled satisfiability under adaptation υ, showing c.u.s. can fail for that adaptation and σδ,z.The construction uses a fresh proposition x to distinguish the dense-time behavior from the sampled behavior.Source: §3.3.3 · p. 23
  • For modalities U↓, S↓, R, and T, the passage states that a regular Z-to-R adaptation preserving c.u.i.s. for every discrete-endpoint formula entails c |=R ηZ.Source: §3.3.3 · p. 23

3.4 Generalizations

The section extends sampling-invariance results beyond flat MTL, using shiftability to identify nestable formulas. It shows that LTL formulas are shiftable and can be nested within flat MTL without losing continuous-to-discrete sampling invariance.

3.4 Generalizations

  • For any sampling period δ, a proposition holding on an interval longer than δ but shorter than 2δ can be sampled at only one instant for some offset, so the example formula is not sampling invariant.The formula requires the proposition to hold at two adjacent sampling instants.Source: §3.4 · p. 24

3.4.1 Shiftable Formulas

  • Shiftability lets formulas containing a shiftable subformula be flattened using an equivalent auxiliary proposition, supporting larger sampling-invariant and inverse-sampling-invariant MTL fragments.Theorem 21 establishes these results for {ψ}-♭MTL when ψ is shiftable.Source: §3.4.1 · pp. 24–25

3.4.2 LTL is Nestable

  • All LTL formulas are shiftable, and all LTL-♭MTL formulas are sampling invariant, so qualitative LTL formulas can be nested within ♭MTL.The result depends on non-strict LTL operators; a similar corollary for inverse sampling invariance does not follow by the same argument.Source: §3.4.2 · pp. 25–26

4 Verification via Sampling

Sampling invariance connects non-Berkeley dense-time semantics with discrete-time semantics and supports analysis at their interface. The paper applies this connection to a partial verification technique that analyzes discrete-time samplings and transfers results back to dense time under restrictions.

4 Verification via Sampling

  • Sampling invariance rigorously relates non-Berkeley dense-time semantics to discrete-time semantics, supporting descriptions of interacting components and refinements from physical dense-time models to implementable discrete-time models.The paper presents these as applications of the sampling theory.Source: §4 · p. 26
  • The verification technique analyzes discrete-time samplings of dense-endpoint ♭MTL formulas and transfers results back to dense time under restrictions.Under- and over-approximations support a partial reduction to discrete-endpoint MTL validity checking.Source: §4 · pp. 26–27

4.1 Under- and Over- Approximations

For dense-endpoint ♭MTL formulas, the paper constructs discrete-time under- and over-approximations that preserve complementary validity information. Their use is restricted to sampling periods compatible with the formula's interval bounds.

4.1 Under- and Over- Approximations

  • The approximation mappings take dense-endpoint ♭MTL formulas to discrete-endpoint formulas, allowing dense-time validity to be inferred from validity of their approximations.The over-approximation is described as a sort of inverse of the canonical adaptation ηZδ.Source: §4.1 · p. 27

4.1.1 Granularity

  • A sampling period δ belongs to Dφ when every interval bound in φ divided by δ is an integer; Dφ has a maximum but no minimum.The granularity ρφ is defined from the irreducible interval endpoints using their greatest common divisor and least common multiple.Source: §4.1.1 · p. 27

4.1.2 Under-Approximation

  • The under-approximation preserves counterexamples: if a discrete behavior fails Ωδ[φ], every corresponding non-Berkeley dense-time behavior fails φ.It is defined for δ in Dφ, where it coincides with the canonical adaptation ηRδ.Source: §4.1.2 · pp. 27–28

4.1.3 Over-Approximation

  • The over-approximation preserves satisfaction: if a discrete behavior satisfies Oδ[φ], every corresponding non-Berkeley dense-time behavior satisfies φ.It is defined for δ in Dφ and is a pseudo-inverse of ηZδ.Source: §4.1.3 · p. 28

4.2 MTL Verification

The verification procedure reduces checking dense-time ♭MTL system properties to discrete-time validity checks using under- and over-models. It is incomplete: it considers only behaviors constrained by the chosen sampling period and can return no conclusion when the models do not settle the check.

4.2 MTL Verification

  • Verification of a system against a property is expressed as validity of Alw(φsys) ⇒ Alw(φprop), with validity meaning every system behavior satisfies the requirements.A failure of validity indicates a system behavior violating the requirements.Source: §4.2 · p. 29

4.2.1 Verification Algorithm

  • The algorithm checks discrete-time validity of over- and under-model implications to return success, failure, or fail, with correctness following from Proposition 26.The procedure assumes δ belongs to the permitted granularity set for the system and property formulas.Source: §4.2.1 · pp. 29–30

4.2.2 Incompleteness

  • The algorithm is incomplete because it covers only non-Berkeley behaviors for the chosen δ and because the under- and over-models may leave the verification result inconclusive.Trying smaller δ does not guarantee even the stated partial completeness condition.Source: §4.2.2 · p. 30

4.3 Discussion

The discussion argues that discretization can make dense-time MTL verification more practical by using discrete-time verification tools. It also shows how reformulating a model can make incomplete approximations more useful, though the reformulation effort can be non-trivial.

4.3 Discussion

  • Discrete-time verification offers off-the-shelf tools where dense-time temporal-logic decision procedures remain scarce, motivating discretization as a practical route.The authors report that related work implemented their procedure and demonstrated practical efficiency on non-trivial verification examples [FPR08b] [BFPR09].Source: §4.3 · pp. 31–32
  • The flat MTL fragment retains enough expressive power under global satisfiability to describe typical real-time behaviors, including timed automata and bounded time Petri nets.The cited examples require careful formalization to avoid inconsistencies; the experience can extend to systems described using states and transitions [FPR08b] [BFPR09].Source: §4.3 · p. 32
  • Reformulating dense-time models can reduce the practical impact of incompleteness, but the additional modeling effort can be non-trivial.Equivalent dense-endpoint formulas may yield nonequivalent discrete-time under- or over-approximations.Source: §4.3 · p. 32
  • For the example system, proving φO Z-valid for any δ = 1/k verifies the system over dense time.The passage characterizes this as an accurate discrete-time rendition of the dense-time model.Source: §4.3 · p. 32
  • An equivalent reformulation of φprop changes its over-approximation from ¬p to a non-trivially satisfiable condition for any k > 1.The passage presents this as a way to avoid an unsatisfactory approximation when using an under-model.Source: §4.3 · p. 32

5 Related Work

The related-work discussion compares sampling with digitization and other approaches to connecting dense- and discrete-time semantics. It also relates the paper’s information-loss account to classical signal sampling while distinguishing the settings.

5.1 Comparison with Digitization

  • Digitization and sampling address dense-to-discrete verification, but differ in semantic structures versus timed words and in semantic versus syntactic criteria.The section frames digitizability and sampling invariance as properties of timed-word sets and formulas, respectively.Source: §5.1 · p. 33
  • Digitizability and sampling invariance define incomparable formula classes, so their verification techniques may offer complementary strengths and weaknesses.Each class contains formulas that are not in the other.Source: §5.1 · p. 34

5.2 Other Work on the Relations between Dense and Discrete Time

  • Prior digitization work spans timed automata, CSP, and duration-calculus variants, with approaches using closure properties or approximations to connect dense- and discrete-time verification.The cited duration-calculus approach uses α+ and α− approximations and is incomplete because dense-time DC is undecidable.Source: §5.2 · p. 35
  • Other related methods use finite variability for dense-to-discrete correspondence or analyze continuous-time system behavior through discrete signal samples.The latter approach shares motivations and ideas with this paper but has a complementary scope.Source: §5.2 · p. 36

5.3 The Sampling Theorem

  • Classical sampling theory guarantees perfect signal reconstruction when δ < 1/(2Bs), where Bs is the signal’s highest frequency.The paper notes that its Boolean-valued dense-time behaviors have infinite bandwidth because of transition discontinuities, so the classical theorem does not strictly apply.Source: §5.3 · p. 36
  • For the step-signal example, sampling loses the exact switch location within (−δ, δ), and the Whittaker-Shannon reconstruction deviates there while nearly matching elsewhere.Figure 4 identifies s(t) in gray and its reconstruction bs(t) in black.Source: §5.3 · p. 37, Figure 4 · p. 37

6 Conclusion

The paper presents an approach relating dense-time MTL formulas to discrete-time counterparts and uses it for verification through discretization. The technique is inherently incomplete, although it has yielded promising results in practice.

6 Conclusion

  • The paper relates dense-time MTL formulas to discrete-time counterparts and uses that relationship for system verification through discretization.The technique is inherently incomplete, though it has yielded promising practical results [FPR08b] [BFPR09].Source: §6 · p. 37
  • Future work will apply sampling to synthesize real-time software components from continuous-time specifications and further characterize or reduce verification incompleteness.Source: §6 · p. 37
Loading 0911.5642v2…