pith. sign in

arxiv: 2606.28429 · v1 · pith:CCQ33PO6new · submitted 2026-06-25 · 💻 cs.LO · cs.MA

An Algebraic Framework for Quantitative Semantics of Spatio-Temporal Logic with Graph Operators

Sheryl Paul , Vidisha Kudalkar , Anand Balakrishnan , Tianhao Wu , Lars Lindemann , Jyotirmoy V. Deshmukh This is my paper

Pith reviewed 2026-06-30 00:28 UTC · model grok-4.3

classification 💻 cs.LO cs.MA
keywords Spatio-Temporal LogicQuantitative SemanticsGraph OperatorsSTL-GOAlgebraic FrameworkMulti-agent SystemsMonotonicity
0
0 comments X

The pith

Quantitative semantics for Spatio-Temporal Logic with Graph Operators follow from monotonicity on an abstract accumulator that separates temporal and graph layers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper builds quantitative semantics for STL-GO by layering temporal aggregation apart from graph-operator aggregation. Graph operators, which count neighboring agents, are handled by an abstract accumulator whose fold and readout must be monotone. Soundness and completeness of the semantics hold exactly when these monotonicity conditions are satisfied. The construction is instantiated in Boolean, min-max, signed-deficit, and hybrid forms and tested on multi-agent systems with Dubins-car and satellite dynamics to illustrate the resulting trade-offs.

Core claim

We develop quantitative semantics for STL-GO as a layered algebraic construction that separates temporal aggregation from graph-operator aggregation (governed by an abstract accumulator with a monotone fold and readout). We prove that soundness and completeness reduce to monotonicity conditions on these components.

What carries the argument

Abstract accumulator whose fold and readout functions satisfy monotonicity, governing graph-operator aggregation separately from the temporal layer.

If this is right

  • The framework supports four semantic instantiations (Boolean, min-max, signed-deficit, hybrid) whose quantitative values differ while preserving soundness under monotonicity.
  • Evaluation on a 2D bounded region with stochastic Dubins-car dynamics and a 3D Earth-satellite system demonstrates scalability with the number of agents and time horizon.
  • Accumulator choice controls the numerical interpretation of counting constraints without altering the underlying Boolean semantics when monotonicity holds.
  • The separation of layers allows independent replacement of the temporal or graph aggregation components.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The monotonicity template could be reused to define quantitative semantics for other temporal logics that incorporate counting or aggregation operators.
  • Automated checks for monotonicity on custom fold and readout functions would make the framework easier to extend to new accumulators.
  • The same layered construction might accommodate additional spatial or probabilistic operators while retaining the soundness proof structure.

Load-bearing premise

The graph-operator aggregation can be captured by an abstract accumulator whose fold and readout functions satisfy monotonicity, and that this separation from the temporal layer preserves the intended counting semantics for STL-GO formulas.

What would settle it

An STL-GO formula together with a non-monotone accumulator for which the quantitative semantics nevertheless satisfies soundness or completeness on all input traces.

Figures

Figures reproduced from arXiv: 2606.28429 by Anand Balakrishnan, Jyotirmoy V. Deshmukh, Lars Lindemann, Sheryl Paul, Tianhao Wu, Vidisha Kudalkar.

Figure 1
Figure 1. Figure 1: Limitations of existing spatio-temporal robustness semantics. (a) Both scenarios satisfy “at least 3 neighbors satisfy φ,” but A has zero spare neighbors and B has two; min-max robustness assigns both the same value. STREL cannot express this counting requirement. (b) The dashed-border agent satisfies φ but lies just outside range (d1=R+0.01); the faded agent is far beyond d2 = R + 10. Both are treated the… view at source ↗
Figure 2
Figure 2. Figure 2: (a) Environment 1: 50x50 space with 100 agents, (b) Environment 2: 3D [PITH_FULL_IMAGE:figures/full_fig_p013_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Robustness values across semantics for a sampled trajectory. Alternating Spatio-temporal opera￾tors (φ r-sp ℓ ): These specifications (Eq. 3) interleave spatial and temporal operators in alternation over G dist t , G sense t , G comm t graphs with edge-count bound E = [1, 20] and weight interval W = [0, 20]. At each nesting level ℓ, a temporal opera￾tor T = {F, G} is applied first, fol￾lowed by a spatial o… view at source ↗
read the original abstract

Spatio-Temporal Logic with Graph Operators (STL-GO) extends Signal Temporal Logic (STL) to multi-agent systems via graph operators that count neighboring agents satisfying a property, together with multi-agent quantifiers. While Boolean semantics for STL-GO are well-defined, quantitative semantics have not yet been developed and existing quantitative semantics for spatio-temporal logics such as STREL cannot capture the counting constraints in STL-GO's graph operators. We develop quantitative semantics for STL-GO as a layered algebraic construction that separates temporal aggregation from graph-operator aggregation (governed by an abstract accumulator with a monotone fold and readout). We prove that soundness and completeness reduce to monotonicity conditions on these components. We implement the framework and evaluate it on two multi-agent environments: a 2D bounded region with stochastic Dubins-car dynamics and a 3D Earth-satellite system, under four semantic instantiations (Boolean, min-max, signed-deficit, and a hybrid), demonstrating the tradeoffs between accumulator choices and reporting scalability in the number of agents and time horizon.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper develops quantitative semantics for Spatio-Temporal Logic with Graph Operators (STL-GO) via a layered algebraic construction that separates temporal aggregation from graph-operator aggregation, the latter governed by an abstract accumulator equipped with a monotone fold and readout. It claims that soundness and completeness of the resulting quantitative semantics reduce to monotonicity conditions on these accumulator components, and reports an implementation evaluated on a 2D Dubins-car system and a 3D Earth-satellite system under four semantic instantiations (Boolean, min-max, signed-deficit, hybrid).

Significance. If the reduction to monotonicity holds with the stated assumptions, the framework supplies a modular, reusable way to lift Boolean STL-GO semantics to quantitative ones while preserving counting constraints on graph neighborhoods; the explicit separation of layers and the four concrete instantiations provide a clear basis for comparing trade-offs in multi-agent verification.

major comments (2)
  1. [reduction theorem (Section 4)] The central claim (abstract and the reduction theorem) that soundness and completeness reduce to monotonicity of the fold and readout is load-bearing yet appears incomplete: monotonicity alone permits saturating or constant-on-positive folds that map every count meeting a threshold to the same non-positive value, violating completeness for the intended counting semantics of STL-GO graph operators. The manuscript must either add an explicit extra axiom (e.g., strict increase past the threshold or unbounded range) or demonstrate why the existing monotone-fold definition already guarantees positive outputs for satisfying counts.
  2. [§3.2] §3.2 (accumulator definition): the weakest assumption—that an arbitrary monotone accumulator can faithfully encode the exact counting thresholds of STL-GO graph operators—is not discharged by the monotonicity conditions alone; an edge case where the fold saturates below the required positive readout would falsify completeness while still satisfying the stated hypotheses.
minor comments (2)
  1. [Abstract] The abstract states that soundness and completeness proofs 'reduce to monotonicity conditions' but does not list the precise monotonicity axioms; a one-sentence enumeration would improve readability.
  2. [experimental evaluation] Table 1 (or the corresponding experimental table) reports scalability in number of agents and time horizon; adding a column for the concrete accumulator parameters used in each of the four instantiations would make the trade-off discussion easier to reproduce.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review. The two major comments both concern the sufficiency of the stated monotonicity conditions for the reduction theorem. We address them point by point below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [reduction theorem (Section 4)] The central claim (abstract and the reduction theorem) that soundness and completeness reduce to monotonicity of the fold and readout is load-bearing yet appears incomplete: monotonicity alone permits saturating or constant-on-positive folds that map every count meeting a threshold to the same non-positive value, violating completeness for the intended counting semantics of STL-GO graph operators. The manuscript must either add an explicit extra axiom (e.g., strict increase past the threshold or unbounded range) or demonstrate why the existing monotone-fold definition already guarantees positive outputs for satisfying counts.

    Authors: We agree that the current formulation of monotonicity alone does not rule out saturating folds that could map all satisfying counts to a non-positive value, thereby breaking completeness. The manuscript will be revised by adding an explicit axiom to the accumulator definition (Section 3.2) requiring that the readout is strictly positive whenever the fold value meets or exceeds the counting threshold of the graph operator. The reduction theorem in Section 4 will be restated to include this axiom, and the proof will be updated to invoke it explicitly. This change preserves the layered algebraic structure while closing the identified gap. revision: yes

  2. Referee: [§3.2] §3.2 (accumulator definition): the weakest assumption—that an arbitrary monotone accumulator can faithfully encode the exact counting thresholds of STL-GO graph operators—is not discharged by the monotonicity conditions alone; an edge case where the fold saturates below the required positive readout would falsify completeness while still satisfying the stated hypotheses.

    Authors: We concur that the existing monotonicity hypotheses do not by themselves discharge the requirement that every monotone accumulator faithfully encodes the counting thresholds. We will strengthen the accumulator definition in §3.2 with an additional axiom ensuring that the fold is unbounded above the threshold (or at minimum produces a readout strictly above zero for satisfying counts). The four concrete instantiations will be checked against the new axiom, and the completeness direction of the reduction theorem will be adjusted to rely on it. This revision directly addresses the edge-case concern. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper defines quantitative semantics for STL-GO via a layered algebraic construction that takes an abstract accumulator (with monotonicity assumptions on its fold and readout) as an independent input. Soundness and completeness are then shown to follow from those stated assumptions. No equations reduce the central result to a self-definition, a fitted parameter renamed as prediction, or a load-bearing self-citation chain. The monotonicity conditions are explicit premises, not derived from the target semantics, so the framework does not collapse by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the introduction of an abstract accumulator whose monotonicity properties are required for the soundness proofs; this is a domain assumption for the semantics rather than a derived fact. No numerical free parameters are mentioned.

axioms (1)
  • domain assumption The accumulator component admits a monotone fold and a monotone readout
    The abstract states that soundness and completeness proofs reduce exactly to these monotonicity conditions on the accumulator.
invented entities (1)
  • Abstract accumulator with monotone fold and readout no independent evidence
    purpose: To separate and govern graph-operator aggregation independently of temporal aggregation while handling counting constraints
    Introduced as the governing component of the layered construction; no independent evidence outside the framework is provided in the abstract.

pith-pipeline@v0.9.1-grok · 5737 in / 1470 out tokens · 52048 ms · 2026-06-30T00:28:19.433805+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

37 extracted references · 14 canonical work pages · 3 internal anchors

  1. [1]

    Akazaki, T., Hasuo, I.: Time robustness in mtl and expressivity in hybrid system falsification.In:InternationalConferenceonComputerAidedVerification.pp.356–

  2. [2]

    In: 2021 60th IEEE Conference on Decision and Control (CDC)

    Alsalehi, S., Mehdipour, N., Bartocci, E., Belta, C.: Neural network-based control for multi-agent systems from spatio-temporal specifications. In: 2021 60th IEEE Conference on Decision and Control (CDC). pp. 5110–5115. IEEE (2021)

    2021

  3. [3]

    Flightgoggles: Photorealistic sensor simulation for perception -driven robotics using photogrammetry and virtual reality

    Balakrishnan, A., Deshmukh, J.V.: Structured reward shaping using signal tem- poral logic specifications. In: 2019 IEEE/RSJ International Conference on Intelli- gent Robots and Systems (IROS). pp. 3481–3486 (2019). https://doi.org/10.1109/ IROS40897.2019.8968254

    work page arXiv 2019

  4. [4]

    In: Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control

    Balakrishnan, A., Jaksic, S., Aguilar, E., Nickovic, D., Deshmukh, J.: Poster abstract: Model-free reinforcement learning for symbolic automata-encoded ob- jectives. In: Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control. HSCC ’22, Association for Computing Ma- chinery, New York, NY, USA (2022). https://doi.org...

    work page doi:10.1145/3501710.3524734 2022

  5. [5]

    In: Pro- ceedings of the 28th ACM International Conference on Hybrid Systems: Computa- tionandControl.HSCC’25,AssociationforComputingMachinery,NewYork,NY, USA (2025)

    Balakrishnan, A., Paul, S., Silvetti, S., Nenzi, L., Deshmukh, J.V.: Monitoring spa- tially distributed cyber-physical systems with alternating finite automata. In: Pro- ceedings of the 28th ACM International Conference on Hybrid Systems: Computa- tionandControl.HSCC’25,AssociationforComputingMachinery,NewYork,NY, USA (2025). https://doi.org/10.1145/37168...

    work page doi:10.1145/3716863.3718033 2025

  6. [6]

    In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design

    Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spa- tially distributed cyber-physical systems. In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design. pp. 146–155. MEMOCODE ’17, Association for Computing Machinery, New York, NY, USA (Sep 2017). https://doi.org/10.1145/312704...

    work page doi:10.1145/3127041.3127050 2017

  7. [7]

    On the Robustness of Temporal Properties for Stochastic Models

    Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: On the robustness of tem- poral properties for stochastic models. arXiv preprint arXiv:1309.0866 (2013)

    work page internal anchor Pith review Pith/arXiv arXiv 2013

  8. [8]

    In: International Conference on Formal Modeling and Analysis of Timed Systems

    Chen, H., Lin, S., Smolka, S.A., Paoletti, N.: An stl-based formulation of resilience in cyber-physical systems. In: International Conference on Formal Modeling and Analysis of Timed Systems. pp. 117–135. Springer (2022)

    2022

  9. [9]

    Journal of the Australian Mathematical Society34(3), 377–393 (Jun 1983)

    Cignoli, R., Gallego, M.S.D.: Dualities for some de morgan algebras with operators and lukasiewicz algebras. Journal of the Australian Mathematical Society34(3), 377–393 (Jun 1983). https://doi.org/10.1017/S1446788700023806

    work page doi:10.1017/s1446788700023806 1983

  10. [10]

    In: Chatterjee, K., Henzinger, T.A

    Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued sig- nals. In: Chatterjee, K., Henzinger, T.A. (eds.) Formal Modeling and Analysis of Timed Systems. pp. 92–106. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15297-9_9

    work page doi:10.1007/978-3-642-15297-9_9 2010

  11. [11]

    Theoretical Computer Science410(42), 4262–4291 (Sep 2009)

    Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science410(42), 4262–4291 (Sep 2009). https://doi.org/10.1016/j.tcs.2009.06.021

    work page doi:10.1016/j.tcs.2009.06.021 2009

  12. [12]

    The First-Order Logic of Hyperproperties

    Finkbeiner, B., Zimmermann, M.: The first-order logic of hyperproperties. arXiv preprint arXiv:1610.04388 (2016)

    work page internal anchor Pith review Pith/arXiv arXiv 2016

  13. [13]

    Springer Netherlands, Dordrecht (1999)

    Golan, J.S.: Semirings and Their Applications. Springer Netherlands, Dordrecht (1999). https://doi.org/10.1007/978-94-015-9333-5

    work page doi:10.1007/978-94-015-9333-5 1999

  14. [14]

    In: Proceedings of 18 Paul, Kudalkar & Balakrishnan et.al

    Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Gros, R., Belta, C.: Spatel: a novel spatial-temporal logic and its applications to networked systems. In: Proceedings of 18 Paul, Kudalkar & Balakrishnan et.al. the 18th International Conference on Hybrid Systems: Computation and Control. pp. 189–198 (2015)

    2015

  15. [15]

    In: 2019 IEEE 58th Conference on Decision and Control (CDC)

    Haghighi, I., Mehdipour, N., Bartocci, E., Belta, C.: Control from signal temporal logic specifications with smooth cumulative quantitative semantics. In: 2019 IEEE 58th Conference on Decision and Control (CDC). pp. 4361–4366. IEEE (2019)

    2019

  16. [16]

    Formal Methods in System Design53(1), 83–112 (Aug 2018)

    Jakšić, S., Bartocci, E., Grosu, R., Nguyen, T., Ničković, D.: Quantitative moni- toring of stl with edit distance. Formal Methods in System Design53(1), 83–112 (Aug 2018). https://doi.org/10.1007/s10703-018-0319-x

    work page doi:10.1007/s10703-018-0319-x 2018

  17. [17]

    arXiv preprint arXiv:2511.08502 (2025)

    Karagulle, R., Vasile, C.I., Ozay, N.: Safe and optimal learning from preferences via weighted temporal logic with applications in robotics and formula 1. arXiv preprint arXiv:2511.08502 (2025)

    work page arXiv 2025

  18. [18]

    In: International Conference on Runtime Verification

    Kudalkar, V., Hashemi, N., Mukhopadhyay, S., Mallick, S., Budnik, C., Nagaraja, P., Deshmukh, J.V.: Sampling-based and gradient-based efficient scenario gener- ation. In: International Conference on Runtime Verification. pp. 70–88. Springer (2024)

    2024

  19. [19]

    In: Proceedings of the International Conference on Automated Planning and Schedul- ing

    Kudalkar, V., Ponguluri, S., Balakrishnan, A., Deshmukh, J.V.: Sampling-based multi-agent path planning guided by spatio-temporal logic mission objectives. In: Proceedings of the International Conference on Automated Planning and Schedul- ing. vol. 36, pp. 133–141 (2026)

    2026

  20. [20]

    Springer Berlin Heidel- berg, Berlin, Heidelberg (1986)

    Kuich, W., Salomaa, A.: Semirings, Automata, Languages. Springer Berlin Heidel- berg, Berlin, Heidelberg (1986)

    1986

  21. [21]

    In: 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)

    Li, X., Vasile, C.I., Belta, C.: Reinforcement learning with temporal logic rewards. In: 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). pp. 3834–3839. IEEE (2017)

    2017

  22. [22]

    In: 2020 ACM/IEEE 11th International Conference on Cyber-Physical Systems (ICCPS)

    Ma, M., Bartocci, E., Lifland, E., Stankovic, J., Feng, L.: Sastl: Spatial aggregation signal temporal logic for runtime monitoring in smart cities. In: 2020 ACM/IEEE 11th International Conference on Cyber-Physical Systems (ICCPS). pp. 51–62. IEEE (2020)

    2020

  23. [23]

    In: Lakhnech, Y., Yovine, S

    Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. pp. 152–166. Springer Berlin Heidelberg, Berlin, Heidelberg (2004)

    2004

  24. [24]

    In: 2019 American Control Con- ference (ACC)

    Mehdipour, N., Vasile, C.I., Belta, C.: Arithmetic-geometric mean robustness for control from signal temporal logic specifications. In: 2019 American Control Con- ference (ACC). pp. 1690–1695. IEEE (2019)

    2019

  25. [25]

    Logical Methods in Computer ScienceVolume 18, Issue 1(Jan 2022)

    Nenzi, L., Bartocci, E., Bortolussi, L., Loreti, M.: A logic for monitoring dy- namic networks of spatially-distributed cyber-physical systems. Logical Methods in Computer ScienceVolume 18, Issue 1(Jan 2022). https://doi.org/10.46298/ lmcs-18(1:4)2022

    2022

  26. [26]

    Logical Methods in Computer ScienceVolume 14, Issue 4(Oct 2018)

    Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties with sstl. Logical Methods in Computer ScienceVolume 14, Issue 4(Oct 2018). https://doi.org/10.23638/ LMCS-14(4:2)2018, https://lmcs.episciences.org/4913

    2018

  27. [27]

    In: 2017 IEEE Conference on Control Tech- nology and Applications (CCTA)

    Pant, Y.V., Abbas, H., Mangharam, R.: Smooth operator: Control using the smooth robustness of temporal logic. In: 2017 IEEE Conference on Control Tech- nology and Applications (CCTA). pp. 1235–1240. IEEE (2017)

    2017

  28. [28]

    In: Hillston, J., Soudjani, S., Waga, M

    Paul, S., Balakrishnan, A., Qin, X., Deshmukh, J.V.: Multi-agent path finding for timed tasks using evolutionary games. In: Hillston, J., Soudjani, S., Waga, M. (eds.) Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems. pp. 302–321. Springer Nature Switzerland, Cham (2024) Quantitative Semantics for STL-GO 19

    2024

  29. [29]

    IOS Press (Oct 2024)

    Paul, S., Deshmukh, J.V.: Survival of the Fittest: Evolutionary Adaptation of Policies for Environmental Shifts. IOS Press (Oct 2024). https://doi.org/10.3233/ faia240874, http://dx.doi.org/10.3233/FAIA240874

    work page doi:10.3233/faia240874 2024

  30. [30]

    In: 53rd IEEE Conference on Decision and Control

    Raman, V., Donzé, A., Maasoumy, M., Murray, R.M., Sangiovanni-Vincentelli, A., Seshia, S.A.: Model predictive control with signal temporal logic specifications. In: 53rd IEEE Conference on Decision and Control. pp. 81–87. IEEE (2014)

    2014

  31. [31]

    In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control

    Rodionova, A., Bartocci, E., Nickovic, D., Grosu, R.: Temporal logic as filtering. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control. pp. 11–20 (2016)

    2016

  32. [32]

    STL-Based Motion Planning and Uncertainty-Aware Risk Analysis for Human-Robot Collaboration with a Multi-Rotor Aerial Vehicle

    Silano, G., Afifi, A., Saska, M., Franchi, A.: Stl-based motion planning and uncertainty-aware risk analysis for human-robot collaboration with a multi-rotor aerial vehicle. arXiv preprint arXiv:2509.10692 (2025)

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  33. [33]

    In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control

    Waga, M.: Falsification of cyber-physical systems with robustness-guided black-box checking. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control. pp. 1–13 (2020)

    2020

  34. [34]

    In: Robotics: Science and Systems (2017)

    Yoo, C., Belta, C.: Rich time series classification using temporal logic. In: Robotics: Science and Systems (2017)

    2017

  35. [35]

    ACM Transactions on Embedded Computing Systems24(5s), 1–23 (2025) 20 Paul, Kudalkar & Balakrishnan et.al

    Zhao, Y., Yu, X., Hoxha, B., Fainekos, G., Deshmukh, J., Lindemann, L.: Stl-go: Spatio-temporal logic with graph operators for distributed systems with multiple network topologies. ACM Transactions on Embedded Computing Systems24(5s), 1–23 (2025) 20 Paul, Kudalkar & Balakrishnan et.al. Appendix A Compositional Behavior of Algebraic Semantics Table 3: Alge...

    2025

  36. [36]

    For every atomic predicateµ,ρ(σ, µ, t)∈K + ⇐ ⇒σ, t|=µ

  37. [37]

    at least 5 neighbors satisfyψ

    for every semantic operatorF:K n →K, there exists a Boolean operator f:{0,1} n → {0,1}such that for all inputsx 1, . . . , xn ∈K, F(x 1, . . . , xn)∈K + ⇐ ⇒f(1 x1∈K + , . . . ,1xn∈K + ) = 1. Then for every formulaϕ,ρ(σ, ϕ, t)∈K + ⇐ ⇒σ, t|=ϕ.That is, the quan- titative semantics are sound and complete with respect to the Boolean semantics. Proof.The proof ...