Quantitative Predictive Monitoring and Control for Safe Human-Machine Interaction

Josephine Lamp; Lu Feng; Matthew B. Dwyer; Meiyi Ma; Sebastian Elbaum; Shuyang Dong

REVIEW 4 major objections 5 minor 29 references

Quantitative Predictive Monitoring and Control for Safe Human-Machine Interaction

T0 review · 4 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A quantitative monitor for Signal Temporal Logic with Uncertainty computes a robustness interval whose sign separates guaranteed, possible, and impossible satisfaction of a safety requirement.

desk verdict Useful interval-based robustness for STL-U flowpipes, but the weak-satisfaction soundness theorem is false as stated. read the letter →

arxiv 2412.13365 v1 pith:3PLS5HWU submitted 2024-12-17 cs.AI cs.HCcs.SYeess.SY

Shuyang Dong , Meiyi Ma , Josephine Lamp , Sebastian Elbaum , Matthew B. Dwyer , Lu Feng This is my paper · ORCID

classification cs.AIcs.HCcs.SYeess.SY

keywords SignalTemporalLogicSTL-UquantitativemonitoringrobustnessdegreeBayesiandeeplearninguncertaintycalibrationadaptivecontrolhuman-machineinteraction

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper tries to establish that safety in human-machine interaction can be managed proactively by assigning a quantitative robustness interval to uncertain predictions about the future. For a flowpipe—a sequence of confidence intervals representing all traces a Bayesian neural network considers likely—it defines an STL-U quantitative monitor that returns the worst-case and best-case degree to which a safety requirement is satisfied or violated. The interval is sound in the sense that its sign separates all-traces-satisfy, some-traces-satisfy, and violation outcomes. The paper then uses these intervals in two ways: a loss function that selects which stochastic-regularization and dropout configuration best calibrates the predictor, and an adaptive controller that adjusts insulin or brake/throttle actions according to the predicted margin. If the claims hold, operators of closed-loop systems can act on graded, early safety warnings instead of a binary flag.

What carries the argument

The central object is the robustness degree interval defined by the paper's STL-U quantitative semantics. A flowpipe $\omega$ is a time-indexed sequence of confidence intervals $[\Phi^-_t(\varepsilon),\Phi^+_t(\varepsilon)]$; the semantics push an atomic predicate through that whole interval at each time and lift every STL-U connective to interval arithmetic: $\min^*$ and $\max^*$ take endpoint-wise minima and maxima, and negation flips the interval. Recursion over this structure yields the monitor of Algorithm 1, with one pass over the flowpipe for each temporal operator. The interval carries the soundness theorem: the signs of the lower and upper endpoints are what separate strong satisfaction, weak satisfaction, and violation, and the magnitude is the actionable margin that the adaptive controllers scale their corrections by.

What would settle it

Take a held-out set of real patient or driving traces, reconstruct for each one the predicted flowpipe using the selected Bayesian model, and count how often the actual future trace leaves the 95% confidence interval; if the empirical coverage is substantially below 95%, the interval is not a valid envelope, so the monitor's soundness conclusions do not transfer from simulation to deployment, and re-running the closed-loop comparison with a wider, distribution-free envelope would show whether the safety gains survive.

Watch

Extended reading notes

Core claim

The central claim is that one interval-valued semantics for STL-U computes, for every formula and every flowpipe, a robustness degree interval $[\underline{\rho},\overline{\rho}]$ whose endpoints are sound certificates of strong and weak satisfaction or violation. The monitor evaluates each atomic predicate over every value inside the flowpipe's confidence interval, takes interval-valued minima and maxima for conjunction, disjunction, and temporal operators, and does so in linear time in the length of the flowpipe. Theorem 1 states that a positive lower bound means every trace in the flowpipe satisfies the formula, a non-positive lower bound rules out strong satisfaction, a positive upper bound guarantees that at least one trace satisfies it weakly, and a non-positive upper bound rules out weak satisfaction. The paper also claims that training-time selection guided by these intervals—through the loss $L_{qt}$, which rewards flowpipes whose robustness sign matches the true trace and whose width stays close to the target—improves requirement-satisfaction F1 over accuracy-based and satisfiability-based baselines, and that closed-loop controllers adapted from the same intervals reduce hazards and increase time-in-range in Type 1 Diabetes and car-following simulator studies.

Load-bearing premise

The load-bearing premise is that the Gaussian confidence interval estimated from 30 Monte Carlo samples is a hard envelope containing every future trace the system could produce.

Editorial extensions

If this is right

A controller can trigger proportionate action now whenever the lower bound of the robustness interval crosses zero, because a hazard is possible within the prediction horizon even if the mean prediction looks safe.
Choosing a Bayesian predictor configuration by this interval-based loss yields higher F1 for requirement satisfaction than choosing by accuracy or by strong/weak satisfaction alone.
Because the monitor is linear in the length of the flowpipe, it can be recomputed at every control cycle, making closed-loop online use feasible.
The same monitor and adaptation pattern transfers across domains: the driving case study shows earlier warnings and fewer acceleration-safety hazards with no loss of average speed.
The interval gives a graded warning, so controllers can scale the size of their correction to the predicted severity instead of using a single threshold.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A natural stress test is to replace the Gaussian Monte Carlo confidence intervals with distribution-free conformal prediction regions; if coverage holds under a weaker assumption, the soundness theorem would survive a broader range of real-world data shifts.
The loss function as defined is used to choose among a fixed set of stochastic-regularization and dropout-rate configurations; one could go further and differentiate through the interval semantics to train the network end-to-end toward robustness-aware predictions.
The interval endpoints could serve as a priority ordering among competing requirements, for example a controller that maximizes the minimum lower bound over all active safety specifications.
Applying the same monitor to other closed-loop human-machine systems should reproduce the pattern of earlier pre-alert times, higher detection F1, and fewer hazards, provided the prediction envelope is well calibrated.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The paper has a genuinely useful idea — quantitative robustness intervals for STL-U over flowpipes — and the empirical work is real, but the central soundness theorem is not sound as stated. The min^*/max^* composition in Definition 1 ignores that atomic predicates at the same time instant evaluate the same signal value, so the interval bounds for conjunctions are not tight and cannot support the claimed weak-satisfaction guarantee.

What is actually new: extending Fainekos–Pappas robustness to flowpipe signals in a simple interval-arithmetic way, using those intervals in a loss function for Bayesian RNN uncertainty calibration, and in adaptive control for T1D and car-following. The paper is clearly written, the two case studies are appropriate, and the strong-satisfaction direction of Theorem 1 (properties 1 and 2) appears correct.

Soft spots, in order of severity. First, the weak-satisfaction direction is false. Take a one-step flowpipe X=[-1,1] and φ=(x>0)∧(x<0). Definition 1 gives ρ=[-1,1], since each atomic robustness is [-1,1] and min^* takes the min of the two upper bounds, still 1. The theorem's property 3 then asserts weak satisfaction, but no trace in the flowpipe satisfies both conjuncts. The appendix only proves property 1; the analogous step for property 3 would need (ω⊨_w φ1 and ω⊨_w φ2) ⇒ ω⊨_w (φ1∧φ2), which is false for the existential reading. This matters because the loss function and the monitor's safety claims lean on the upper bound.

Second, the claimed linear time complexity in Section 3.1 is wrong for the until operator; Algorithm 1 has nested loops over the interval, so it is quadratic in |ω| for a single until. Third, there is no code or data artifact, the F1 metric is defined directly on the same robustness intervals the loss function optimizes, and several controller thresholds are hand-set without sensitivity analysis. The adolescent results are mixed, with F1 lower than baseline for the monitor. Fourth, treating a Gaussian confidence interval from 30 Monte Carlo samples as a hard bound on all future traces is a statistical approximation, not a guarantee; if the Gaussian under-covers, the soundness guarantee does not transfer to the real system.

Bottom line: the paper deserves a serious referee because the problem is relevant and the approach is promising, but the soundness theorem needs correction and the empirical claims need artifacts and sensitivity checks. I would not rely on the weak-satisfaction result as stated.

Referee Report

4 major / 5 minor

Summary. The paper proposes a quantitative predictive monitoring and control framework for human-machine interaction under uncertainty. It defines a quantitative semantics for Signal Temporal Logic with Uncertainty (STL-U) that maps a flowpipe (a sequence of intervals) and a formula to a robustness degree interval, and states a soundness theorem (Theorem 1) asserting that the interval bounds correctly indicate strong/weak satisfaction or violation. The robustness intervals are then used in a loss function to select stochastic regularization techniques and dropout rates for Bayesian RNNs, and in adaptive controllers for Type 1 Diabetes management and semi-autonomous driving. Experiments in two simulators report earlier hazard detection, higher F1 scores, and improved closed-loop safety metrics relative to baselines.

Significance. The framework addresses a practically important problem—runtime safety assurance of human-machine interaction with model uncertainty—and combines formal monitoring, uncertainty calibration, and control in a single pipeline. The two case studies (T1D and CARLA driving) are relevant and the empirical results are suggestive. However, the central theoretical claim of soundness for weak satisfaction is flawed as stated, the complexity claim is incorrect, and the loss-function evaluation is partially aligned with the evaluation metric by construction. These issues limit the current contribution, though the underlying approach is potentially salvageable with substantial revision.

major comments (4)

[Section 3.1, Algorithm 1, until case] Theorem 1, property 3 (ρ_bar > 0 ⇒ weak satisfaction) is unsound for conjunctions when weak satisfaction means 'there exists a trace in the flowpipe satisfying φ', as stated in Section 2.2. Because min^* and max^* compose subformula robustness intervals independently, the monitor can certify weak satisfaction of a conjunction even when no single trace satisfies both conjuncts. Concretely, let the one-step flowpipe be X=[-1,1] and φ=(x>0)∧(x<0), with f1(x)=x and f2(x)=-x. The atomic robustness intervals are both [-1,1], so ρ(φ)=[-1,1] and the upper bound is 1>0; Theorem 1(3) then asserts (ω,t) |=_w φ. Yet no x∈[-1,1] satisfies x>0 and x<0, so no trace of the flowpipe satisfies the conjunction. The appendix proves only property 1; the analogous inductive step for property 3 requires an existential choice of a single trace that is consistent across subformulas, which is exactly what the independent interval composition fails to provide. This is load-bearing because the weak-satisfaction guarantee and the loss function in Eq. (3) rely on these bounds.
[Section 3.1, Algorithm 1, until case] The claim that the monitoring algorithm is 'linear time complexity with respect to the length of the flowpipe, |ω|' is false for the until operator as written. The until case contains nested loops: an outer loop over t′∈(t+I) and an inner loop over t″∈[t,t′], giving Ω(|I|^2) time in the worst case. This is a concrete algorithmic claim in the text and should be corrected; if a linear-time implementation is intended, the until operator needs an incremental or dynamic-programming formulation that avoids rescanning the interval for each t′.
[Section 4.1, Eqs. (1)-(3) and Table 1] The loss function Lqt is defined directly on the robustness interval bounds that are later used to compute the F1 score in RQ1 (a true/false positive is determined by ρ(φ,ω,t)>0 or <0, which is derived from the same ρ used in ηr). Selecting the SRT and dropout rate that minimize Lqt on the validation set is therefore aligned with maximizing the reported F1 score by construction. The observed improvement of Lqt over Lacc and Lsat in Table 1 is expected and does not constitute independent evidence of better uncertainty calibration. Please provide an external evaluation—for example, interval coverage of the ground truth, calibration error, or the downstream safety metrics in RQ3—or explicitly acknowledge that this selection procedure is a metric-fitting criterion.
[Section 2.1 and Definition 1] The flowpipe is defined by Gaussian confidence intervals [Φ^−_t(ε), Φ^+_t(ε)] estimated from 30 Monte Carlo samples, and these intervals are treated as hard bounds on all possible future traces. No coverage guarantee is given, and a Gaussian approximation with 30 samples can substantially under-cover the true predictive distribution. Consequently, even if Theorem 1 is true with respect to the abstract flowpipe, it does not provide a soundness guarantee for the real physical system unless the flowpipe provably contains all possible futures. Please add a statistical coverage analysis (e.g., conformal prediction or empirical calibration on held-out data) or state this as an explicit limitation of the safety claim.

minor comments (5)

[Section 3.1, notation] The definitions of min^* and max^* use visually similar symbols for lower and upper interval bounds; please use explicit notation such as \underline{v} and \overline{v} to avoid ambiguity.
[Section 3.2, Eq. (1)] In Eq. (1), the condition \hat{\omega} |=_s φ is applied to a concrete target trace, while strong satisfaction is defined for flowpipes; clarify that the trace is treated as a singleton flowpipe and state which robustness bound is selected in each branch.
[Abstract and Section 3.2] The abstract says the loss function calibrates uncertainty 'during training,' but Section 3.2 uses it only to select an SRT and dropout rate on the validation set after training; please rephrase to accurately describe the selection procedure.
[Section 4.3, Figure 5] The hazard reduction for adolescents (p=0.09) and children (p=0.33) is not statistically significant; the text should qualify the claim that the proposed approach 'reduces the average number of hazards' for all three populations, or present additional evidence of a clinically meaningful effect.
[Algorithms 2 and 3] There are several typos in variable names: 'bolusF lag' should be 'bolusFlag', and 'V iolationOnDeceleration' should be 'ViolationOnDeceleration' (similarly for other violation cases).

Circularity Check

1 steps flagged · score 4.0 of 10

Mild metric-fitting circularity in the RQ1 loss-function evaluation: the F1 metric is defined on the same robustness intervals that Lqt optimizes, but the central monitor soundness and closed-loop safety results are independent.

fitted input called prediction [Section 3.2 (Eq. 3) and Section 4.1 (F1 score definition)]
"Lqt(ω, ˆω, φ) = −β · ηr(ω, ˆω, φ) + (1 − β) · ηd(ω, ˆω) ... ηr(ω, ˆω, φ) = ρ(φ, ω, t) , ˆω |=s φ; −ρ(φ, ω, t) , ˆω ̸|=s φ ... TP denotes the number of true positives (i.e., when the target trace satisfies φ and the predicted flowpipe ω yields ρ(φ, ω, t) > 0)."

The F1 metric's TP/FP/FN are defined by the sign of the same robustness bound ρ(φ,ω,t) that appears in the loss function's first term ηr as ±ρ(φ,ω,t) depending on whether the target satisfies φ. Selecting SRT and dropout rate to minimize Lqt therefore directly pushes ρ toward the sign that counts as correct in F1, so the reported F1 improvement of Lqt over Lsat is partly baked into the objective. This is a metric-alignment/surrogate-optimization issue rather than a full logical equivalence; the monitor soundness theorem and closed-loop hazard/time-in-range evaluations do not reduce to this fit.

full rationale

The paper's central derivation is the STL-U quantitative monitor (Definition 1, Algorithm 1, Theorem 1). This is a new compositional interval semantics, not a restatement of its inputs; the lower/upper robustness bounds are defined independently of the strong/weak satisfaction relations and then claimed sound. The STL-U syntax and strong/weak semantics are cited from Ma et al. 2021, which includes overlapping authors, but that prior work is external and not the target result, so it is not load-bearing circularity. The adaptive controller and the closed-loop T1D and CARLA evaluations use external simulators and clinical metrics (time-in-range, hazard counts, following distance) that are independent of the robustness intervals used for control. The one significant evidential weakness is the RQ1 F1 evaluation: the metric is defined on the same robustness intervals that Lqt optimizes, so the comparison to Lsat is partially self-confirming. Separately, Appendix A states that properties 2-4 of Theorem 1 'can be proved similarly,' but property 3 (weak satisfaction for conjunctions) is not analogous and the min*/max* composition can certify weak satisfaction when no single trace satisfies the conjunction; this is a correctness/soundness risk rather than a circularity, and is flagged here per the review rule.

Assumptions & free parameters 4 free parameters · 4 assumptions · 0 invented entities

The paper introduces no new physical entities. The key free parameters are the loss weight beta, confidence level, dropout rate, and controller thresholds. The main assumptions are the validity of the STL-U base logic, the Gaussian approximation of flowpipes, computability of interval min/max for predicates, and simulator fidelity.

free parameters (4)

beta (loss function weight) = 0.5
The linear combination weight in Lqt is fixed to 0.5 for all experiments; no sensitivity analysis is reported.
confidence level epsilon = 95%
The flowpipe confidence interval is set to 95% in experiments, affecting width of the predicted interval and monitoring results.
dropout rate = 0.8, 0.9, etc.
Selected via validation using the proposed loss function; this is a model selection parameter fitted to data.
adaptive controller thresholds = -20, -70, 0.8, 1.2, 1.5, K=45; CARLA: rho_thre=-3.0, rho_corr=-3.0, minSpeed=5, etc.
Thresholds in Algorithms 2 and 3 are hand-set values based on medical guidelines or heuristic choices, with no sensitivity analysis.

assumptions (4)

domain assumption STL-U syntax and strong/weak satisfaction semantics from Ma et al. 2021
The paper builds directly on the STL-U logic and its satisfaction relations, using them as the foundation for the new quantitative semantics.
domain assumption Gaussian distributions estimated from Monte Carlo samples represent prediction uncertainty
The flowpipe is constructed as confidence intervals from Gaussian fits to 30 MC samples; this assumes the Gaussian approximation captures the true distribution tail behavior.
domain assumption Min and max of atomic predicate f over the flowpipe interval are computable
Definition 1 requires evaluating min and max of f over the continuous interval, which is only straightforward for monotone predicates such as f(x)=x-70; this is not stated explicitly.
domain assumption UVA/PADOVA simulator and CARLA simulator are valid proxies for real human-machine interaction
The evaluation relies on in silico patients and simulated drivers; the paper acknowledges future real-world validation.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Quantitative Predictive Monitoring and Control for Safe Human-Machine Interaction." pith.science (2026). https://pith.science/paper/3PLS5HWU

@misc{pith2026241213365,
  author       = {Pith},
  title        = {Pith review of: Quantitative Predictive Monitoring and Control for Safe Human-Machine Interaction},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3PLS5HWU}},
  note         = {Machine review of arXiv:2412.13365}
}

read the original abstract

There is a growing trend toward AI systems interacting with humans to revolutionize a range of application domains such as healthcare and transportation. However, unsafe human-machine interaction can lead to catastrophic failures. We propose a novel approach that predicts future states by accounting for the uncertainty of human interaction, monitors whether predictions satisfy or violate safety requirements, and adapts control actions based on the predictive monitoring results. Specifically, we develop a new quantitative predictive monitor based on Signal Temporal Logic with Uncertainty (STL-U) to compute a robustness degree interval, which indicates the extent to which a sequence of uncertain predictions satisfies or violates an STL-U requirement. We also develop a new loss function to guide the uncertainty calibration of Bayesian deep learning and a new adaptive control method, both of which leverage STL-U quantitative predictive monitoring results. We apply the proposed approach to two case studies: Type 1 Diabetes management and semi-autonomous driving. Experiments show that the proposed approach improves safety and effectiveness in both case studies.

Figures

Figures reproduced from arXiv: 2412.13365 by the authors.

**Figure 2.** An example flowpipe of predicted BG levels under [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗

**Figure 3.** Adapting control actions based on STL-U quanti [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗

Figures from the paper (2 more)

**Figure 4.** Figure 4: Loss values of using different SRTs and dropout [PITH_FULL_IMAGE:figures/full_fig_p005_4.png]

**Figure 5.** Figure 5: Comparing the number of hazards that occurred [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 26 canonical work pages

[1]

, " * write output.state after.block = add.period write newline

ENTRY address archivePrefix author booktitle chapter edition editor eid eprint howpublished institution isbn journal key month note number organization pages publisher school series title type volume year label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.a...
[2]

write newline

" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...
[3]

American\_Diabetes\_Association. 2022. Standards of Medical Care in Diabetes—2022. Diabetes Care, 45: S17

work page 2022
[4]

Baharisangari, N.; Gaglione, J.-R.; Neider, D.; Topcu, U.; and Xu, Z. 2021. Uncertainty-Aware Signal Temporal Logic Inference. In Software Verification, 61--85. Springer

work page 2021
[5]

A.; Plant, K

Banks, V. A.; Plant, K. L.; and Stanton, N. A. 2018. Driver error or designer error: Using the Perceptual Cycle Model to explore the circumstances surrounding the fatal Tesla crash on 7th May 2016. Safety science, 108: 278--285

work page 2018
[6]

Bartocci, E.; Deshmukh, J.; Donz \'e , A.; Fainekos, G.; Maler, O.; Ni c kovi \'c , D.; and Sankaranarayanan, S. 2018. Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In Lectures on Runtime Verification, 135--175. Springer

work page 2018
[7]

Bengio, Y.; Goodfellow, I.; and Courville, A. 2017. Deep learning. MIT press Cambridge, MA, USA

work page 2017
[8]

L.; Bass, E

Bolton, M. L.; Bass, E. J.; and Siminiceanu, R. I. 2013. Using formal verification to evaluate human-automation interaction: A review. IEEE Transactions on Systems, Man, and Cybernetics: Systems, 43(3): 488--503

work page 2013

Show all 29 references

[9]

CARLATeam. 2023. CARLA 0.9.13 Release. https://carla.org/2021/11/16/release-0.9.13/

2023
[10]

E.; and Pappas, G

Fainekos, G. E.; and Pappas, G. J. 2009. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science, 410(42): 4262--4291

2009
[11]

Feng, L.; Wiltsche, C.; Humphrey, L.; and Topcu, U. 2016. Synthesis of human-in-the-loop control protocols for autonomous systems. IEEE Transactions on Automation Science and Engineering, 13(2): 450--462

2016
[12]

Gal, Y. 2016. Uncertainty in deep learning. Ph.D. thesis, University of Cambridge

2016
[13]

Hochreiter, S.; and Schmidhuber, J. 1997. Long short-term memory. Neural computation, 9(8): 1735--1780

1997
[14]

P.; Breton, M.; Dalla Man, C.; and Cobelli, C

Kovatchev, B. P.; Breton, M.; Dalla Man, C.; and Cobelli, C. 2009. Biosimulation Modeling for Diabetes: In Silico Preclinical Trials: A Proof of Concept in Closed-Loop Control of Type 1 Diabetes. Journal of diabetes science and technology (Online), 3(1): 44

2009
[15]

V.; and Pappas, G

Lindemann, L.; Qin, X.; Deshmukh, J. V.; and Pappas, G. J. 2023. Conformal prediction for STL runtime verification. In Proceedings of the ACM/IEEE 14th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2023), 142--153

2023
[16]

A.; Dixon, C.; and Fisher, M

Luckcuck, M.; Farrell, M.; Dennis, L. A.; Dixon, C.; and Fisher, M. 2019. Formal specification and verification of autonomous robotic systems: A survey. ACM Computing Surveys (CSUR), 52(5): 1--41

2019
[17]

W.; Bailey, R

Lum, J. W.; Bailey, R. J.; Barnes-Lomen, V.; Naranjo, D.; Hood, K. K.; Lal, R. A.; Arbiter, B.; Brown, A. S.; DeSalvo, D. J.; Pettus, J.; et al. 2021. A real-world prospective study of the safety and effectiveness of the loop open source automated insulin delivery system. Diab...

2021
[18]

Ma, M.; Gao, J.; Feng, L.; and Stankovic, J. 2020. STLnet: Signal temporal logic enforced multivariate recurrent neural networks. Advances in Neural Information Processing Systems, 33: 14604--14614

2020
[19]

Ma, M.; Stankovic, J.; Bartocci, E.; and Feng, L. 2021. Predictive monitoring with logic-calibrated uncertainty for cyber-physical systems. ACM Transactions on Embedded Computing Systems (TECS), 20(5s): 1--25

2021
[20]

A.; and Feng, L

Ma, M.; Stankovic, J. A.; and Feng, L. 2021. Toward formal methods for smart cities. Computer, 54(9): 39--48

2021
[21]

Maler, O.; and Nickovic, D. 2004. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, 152--166. Springer

2004
[22]

D.; Micheletto, F.; Lv, D.; Breton, M.; Kovatchev, B.; and Cobelli, C

Man, C. D.; Micheletto, F.; Lv, D.; Breton, M.; Kovatchev, B.; and Cobelli, C. 2014. The UVA/PADOVA type 1 diabetes simulator: new features. Journal of diabetes science and technology, 8(1): 26--34

2014
[23]

Qin, X.; and Deshmukh, J. V. 2020. Clairvoyant Monitoring for Signal Temporal Logic. In International Conference on Formal Modeling and Analysis of Timed Systems, 178--195. Springer

2020
[24]

SafeBenchTeam. 2023. SafeBench: A Benchmark for Evaluating Autonomous Vehicles in Safety-critical Scenarios. https://safebench.github.io/

2023
[25]

Sharp, H.; Preece, J.; and Rogers, Y. 2019. Interaction design: beyond human-computer interaction. NY: Wiley

2019
[26]

Slattery, D.; Amiel, S.; and Choudhary, P. 2018. Optimal prandial timing of bolus insulin in diabetes management: a review. Diabetic Medicine, 35(3): 306--316

2018
[27]

Visconti, E.; Bartocci, E.; Loreti, M.; and Nenzi, L. 2021. Online monitoring of spatio-temporal properties for imprecise signals. In Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, 78--88

2021
[28]

Yang, S.; Zhong, Y.; Feng, D.; Li, R. Y. M.; Shao, X.-F.; and Liu, W. 2022. Robot application and occupational injuries: are robots necessarily safer? Safety science, 147: 105623

2022
[29]

Yoon, H.; and Sankaranarayanan, S. 2021. Predictive runtime monitoring for mobile robots using logic-based bayesian intent inference. In 2021 IEEE International Conference on Robotics and Automation (ICRA), 8565--8571. IEEE

2021

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.

[1] [1]

, " * write output.state after.block = add.period write newline

ENTRY address archivePrefix author booktitle chapter edition editor eid eprint howpublished institution isbn journal key month note number organization pages publisher school series title type volume year label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.a...

[2] [2]

write newline

" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...

[3] [3]

American\_Diabetes\_Association. 2022. Standards of Medical Care in Diabetes—2022. Diabetes Care, 45: S17

work page 2022

[4] [4]

Baharisangari, N.; Gaglione, J.-R.; Neider, D.; Topcu, U.; and Xu, Z. 2021. Uncertainty-Aware Signal Temporal Logic Inference. In Software Verification, 61--85. Springer

work page 2021

[5] [5]

A.; Plant, K

Banks, V. A.; Plant, K. L.; and Stanton, N. A. 2018. Driver error or designer error: Using the Perceptual Cycle Model to explore the circumstances surrounding the fatal Tesla crash on 7th May 2016. Safety science, 108: 278--285

work page 2018

[6] [6]

Bartocci, E.; Deshmukh, J.; Donz \'e , A.; Fainekos, G.; Maler, O.; Ni c kovi \'c , D.; and Sankaranarayanan, S. 2018. Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In Lectures on Runtime Verification, 135--175. Springer

work page 2018

[7] [7]

Bengio, Y.; Goodfellow, I.; and Courville, A. 2017. Deep learning. MIT press Cambridge, MA, USA

work page 2017

[8] [8]

L.; Bass, E

Bolton, M. L.; Bass, E. J.; and Siminiceanu, R. I. 2013. Using formal verification to evaluate human-automation interaction: A review. IEEE Transactions on Systems, Man, and Cybernetics: Systems, 43(3): 488--503

work page 2013