SaSTL: Spatial Aggregation Signal Temporal Logic for Runtime Monitoring in Smart Cities

Eli Lifland; Ezio Bartocci; John Stankovic; Lu Feng; Meiyi Ma

REVIEW 6 major objections 4 minor 41 references

SaSTL: Spatial Aggregation Signal Temporal Logic for Runtime Monitoring in Smart Cities

T0 review · 6 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read SaSTL claims that two spatial operators let a single formula express area-wide city requirements and that a parallel monitor checks them over 10,000 sensors.

desk verdict Useful spatial aggregation/counting extension to STL, but the complexity theorem and pseudocode need repair before the efficiency claims can be taken at face value. read the letter →

arxiv 1908.02366 v5 pith:5QULETAK submitted 2019-08-06 cs.CY cs.SYeess.SY

Meiyi Ma , Ezio Bartocci , Eli Lifland , John Stankovic , Lu Feng This is my paper · ORCID

classification cs.CYcs.SYeess.SY

keywords SaSTLsignaltemporallogicspatialaggregationcountingruntimemonitoringsmartcitiesrequirementspecificationparallel

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

SaSTL is a proposed extension of Signal Temporal Logic with two spatial operators, one that aggregates a measured signal over a distance-bounded neighborhood and one that counts how many locations in that neighborhood satisfy a subformula. The paper's central claim is that these operators let a single formula express real city requirements such as "the average noise level within 1 km of all schools should always stay below 50 dB," which STL, SSTL, and STREL cannot express directly. On a corpus of 1,000 city requirements, the paper reports that SaSTL specifies 950 of them, against 184 for STL and 431 for SSTL and STREL. The monitoring algorithms are claimed to check such formulas over up to 10,000 sensors with complexity $O(|\varphi| T_{\max}(\log n + |L|_{\max}/P))$ on $P$ threads, and the reported timings drop from minutes to seconds in the New York case study. The reason to care is that smart-city monitoring needs exactly this one-formula-for-many-locations expressiveness to be practical at runtime.

What carries the argument

The load-bearing mechanism is the spatial-domain neighbor selector $\mathbb{D}=([d_1,d_2],\psi)$ together with a range-tree index over precomputed weighted distances between locations. The index returns the locations in $\mathbb{D}$ for a given location in $O(\log n + |L_{\mathbb{D}}|)$, and the two new operators reduce over exactly that returned set—one reduce over real values, the other over Booleans. Nested under the STL temporal operators, this gives every SaSTL formula a concrete, finite, queryable spatial footprint, which is what makes the stated complexity bound and the parallel implementation possible.

What would settle it

Have an independent group encode the 467 SaSTL-only requirements in each baseline language using a precise grammar that permits finite conjunctions over locations; if most can be encoded, the claimed 95% coverage advantage is largely an artifact of the one-formula rule. Separately, on a requirement with a large neighborhood, measure wall-clock time at 1, 2, 4, and 8 threads; if the speedup does not approach the $P$-fold reduction in the $|L_{\mathbb{D}}|/P$ term, the parallel complexity bound is not realized in practice.

Watch

Extended reading notes

Core claim

At the center of SaSTL is the spatial domain $\mathbb{D}=([d_1,d_2],\psi)$, which names a ring of locations: those within weighted distance $d_1$ to $d_2$ from the current location and whose point-of-interest labels satisfy $\psi$. The spatial aggregation operator $A^{op}_{\mathbb{D}} x \sim c$ applies $op \in \{\max,\min,\mathrm{sum},\mathrm{avg}\}$ to the non-null readings of signal $x$ from all locations in that ring and compares the result with $c$. The spatial counting operator $C^{op}_{\mathbb{D}} \phi \sim c$ does the same reduce over Boolean satisfaction values of $\phi$ at those locations, so $C^{\mathrm{avg}}_{\mathbb{D}}\phi > 0.9$ is literally "at least 90% of the neighborhood satisfies $\phi$." The paper claims this pair of operators is the missing expressiveness: requirements that previously had to be unrolled one location at a time become single formulas, and the monitor's complexity bound follows from retrieving neighbor sets with range trees and parallelizing the reduce over $P$ threads.

Load-bearing premise

The 95% coverage result rests on a corpus of 1,000 collected requirements and on the coders' rule that a language counts only if it expresses a requirement directly in one formula; if either the corpus or that coding rule is changed, the expressiveness gap over STL, SSTL, and STREL could shrink.

Editorial extensions

If this is right

One formula can now monitor area-wide requirements such as school-zone noise or 90%-of-streets emission limits, replacing per-location formula instantiation.
Monitor runtime grows only logarithmically with the total number of locations plus the largest neighborhood actually visited, so city-scale sensor counts are feasible.
Derived 'everywhere' and 'somewhere' operators follow from counting thresholds, so spatial quantifiers become ordinary STL-style monitoring.
The conflict-detection loop in the New York simulation can re-check predicted futures quickly enough to filter unsafe service requests, which is how the reported safety and environmental improvements arise.

Reading between the lines

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

A natural next step would be to push the aggregation reduce into the sensor network itself, since the neighborhood query is a spatial index lookup and the reduce is associative; this could make the monitor's wall-clock time nearly independent of city size.
The coverage numbers suggest a general pattern: written regulations talk about areas ('within 1 km,' '90% of streets') more often than about discrete points, so any monitoring logic for physical infrastructure probably needs such aggregate operators.
The 95% figure is a claim about a hand-coded corpus; a formal translation benchmark that accepts finite conjunctions as legitimate encodings might produce a different expressiveness ranking, so the gap should be read as provisional.

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

SaSTL gives smart-city monitoring a genuinely useful glue: an operator that aggregates sensor values over a spatial neighborhood and an operator that counts how many neighbors satisfy a subformula. The 1,000-requirement corpus is a real asset, even if it is unpublished and the coding rules need to be public. The core semantics are coherent; the operators are natural extensions of STL rather than a paradigm shift, which is fine.

The paper earns credit for the parallel monitor and for the measured speedups, and NYR1 dropping from 2102s to 26s with 8 threads is plausible. But the efficiency story as printed does not hold up. The stress-test note is right: Theorem 1's bound O(|φ|Tmax(log n + |L|max)) treats each node's cost as one spatial lookup, ignoring that a counting operator evaluates its subformula at every location in its neighborhood. Nested SaSTL formulas, including the paper's own NYR2, can cost |L| times the inner operator cost, so the advertised single-|L|max scale is not established. The proof needs a recurrence with per-node spatial costs, and the prose should either state the product bound or restrict the claim to formulas without spatial nesting.

The pseudocode has material presentation defects. Algorithm 3 calls Monitor on l instead of the neighbor l' inside the loop, which makes the counting semantics unimplementable as written. Algorithm 4's cost-based short-circuit sits after an unconditional return, so it is dead code. Algorithm 5 adds l instead of l' to the task pool. Aggregate and Counting also never skip null ('bot') values even though the semantics says they should. None of these is deeply structural, but they have to be fixed before the algorithms can be considered reference implementations.

On the empirical side: the 95% coverage claim depends on an unpublished corpus and on graduate-student coding with the rule 'directly with one single formula.' That rule can favour SaSTL by construction, because aggregation operators are exactly what SaSTL adds. The authors should publish the corpus, the annotation rules, and ideally the coded formulas. The New York evaluation uses the same group's conflict-resolution framework, which limits external checking; the timing table has no error bars. These are limitations, not fatal flaws.

Who is this for? Researchers in runtime verification and smart-city monitoring who want a practical spatial-temporal logic. I would send it to a serious referee: the core idea is worth engaging, and the revisions are clear. It should not be desk-rejected, but it should not be accepted in this form.

Referee Report

6 major / 4 minor

Summary. SaSTL extends Signal Temporal Logic with a spatial aggregation operator A^op_D x~c and a spatial counting operator C^op_D φ~c, where D is a spatial domain defined by distance bounds and a propositional property over locations. The paper reports a study of over 1,000 quantitatively specified smart-city requirements, claims that 95% of them are expressible in SaSTL versus 18.4% for STL and 43.1% for SSTL/STREL, and presents monitoring algorithms with cost-based parsing and spatial parallelization. The evaluation uses Chicago real-time sensor data and a simulated New York City with up to 10,000 nodes, reporting substantial speedups such as NYR1 dropping from 2102.13 s to 26.12 s with eight threads.

Significance. If the claims held, SaSTL would be a practically useful extension: the two new operators are natural for spatial requirements such as 'average noise within 1 km of every school below 50 dB', and they are not expressible in the cited baselines. The paper's strengths include a self-contained formal syntax and semantics, a large corpus study that identifies an important specification gap, and two substantial case studies with real data. The main weaknesses are technical: the printed monitoring algorithms contain concrete bugs, the complexity theorem does not account for nested spatial operators, and the coverage comparison rests on an unpublished, non-reproducible annotation protocol. These issues are load-bearing for the paper's central scalability and expressiveness claims, but they appear fixable within the scope of a major revision.

major comments (6)

[§V-A, Lemma 1 and Theorem 1] The proof of Theorem 1 bounds the cost of each syntax-tree node by O(Tmax(log n + |L|max)) and then sums over |φ| nodes. This is incorrect for nested spatial operators. A counting operator C^op_D φ evaluates φ at every l′ in L_D (Algorithm 3), so if φ itself contains an aggregation over a neighborhood of size |L′|, the node cost is O(|L_D|(log n + |L′|)), not O(log n + |L|max). NYR2 and NYR4 in Table IV contain exactly this kind of nesting. The advertised complexity O(|φ|Tmax(log n + |L|max)) is therefore not established, and the parallel bound in Lemma 2 inherits the problem. The complexity analysis needs to be revised to account for the product of neighborhood sizes or stated for a restricted class of formulas.
[§V-A, Algorithm 3] In CountingNeighbours, the loop over l′∈L_D calls Monitor(ϕ,ω,t,l,G), using the original location l rather than the neighbor l′. As printed, the counting operator evaluates the subformula repeatedly at the same location and never counts neighboring locations, contradicting the semantics in Section IV-B. The call should be Monitor(ϕ,ω,t,l′,G).
[§V-B, Algorithm 4] Algorithm 4 contains an unconditional 'return Monitor(ϕ1,ω,t,l,G) ∧ Monitor(ϕ2,ω,t,l,G)' before the cost-based branch, making the cost-based short-circuit unreachable. Moreover, the intended short-circuit logic is incorrect: if ¬Monitor(ϕ1) holds, the conjunction is false regardless of ϕ2, so the algorithm should return False, not Monitor(ϕ2). Consequently, the improved parsing optimization described in Section V-B is not implemented by the pseudocode as printed.
[§V-C, Algorithm 5] In the parallel CountingNeighbours, the loop over l′∈L_D uses 'paratasks.add(l)' instead of 'paratasks.add(l′)'. This would enqueue the same outer location repeatedly rather than the neighboring locations, so the parallelization does not distribute the intended monitoring tasks. The fix is to add l′.
[§VI-C, Coverage Analysis] The 95% coverage claim depends on a corpus and a coding rule that are not available for independent verification: 1,000 requirements collected and labeled by graduate students, with 'directly with one single formula' as the criterion, and no reported inter-annotator agreement or release of the corpus. Since this comparison is the main evidence for SaSTL's expressiveness advantage over STL, SSTL, and STREL, the paper should provide the annotated corpus or a detailed auditable protocol, and should report agreement statistics.
[§IV-B, SaSTL Semantics] The treatment of the undefined value bot is contradictory as written. The text first says the satisfaction relation holds only when πv(ω)[t,l]≠bot and αx_D(ω,t,l)≠∅, and then states '(ω,t,l)|=ϕ if πv(ω)[t,l]=bot'. It is also unclear what an aggregation operator should return when the selected set is empty, e.g., Algorithm 2 returns True when n==0. These points need to be resolved because the evaluations use sparse sensor data and the monitor must have a well-defined behavior for missing values.

minor comments (4)

[§V-A] In the bullet list of classical-operator costs, '¬x' should presumably read '¬ϕ' or '¬φ'; the notation is inconsistent with the rest of the section.
[§V-A] The paper states that distances are precomputed and stored in range trees, but the relationship between the weighted graph G and the range-tree representation is not explained; in particular, it is unclear how arbitrary graph distances are answered by a range tree. A brief clarification would help.
[§V-B] After the improved parsing method, the bound is stated with |L′|max, but the notation |L′| is not defined precisely and is easily confused with the earlier |L|max. Please define the effective neighborhood size used in the improved bound.
[§VI-C] The dismissal of SpaTeL in one sentence ('built on a quad tree, and able to specify directions rather than the distance') is too brief for a baseline comparison; at least a short explanation with a reference to this limitation would be fair.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: SaSTL's semantics and monitor are self-contained; the coverage study is empirical and the self-citations are not load-bearing.

full rationale

SaSTL defines its spatial aggregation and counting operators with direct recursive semantics, and the monitoring algorithms are straightforward implementations of those definitions; no parameter is fitted to the outputs the paper claims to predict. The complexity analysis cites an independent range-tree data structure [26], and although Theorem 1's treatment of nested counting operators may have a genuine scaling gap (the inner formula can be re-evaluated at each outer neighbor), that is a technical correctness concern rather than a circular reduction: the bound is not made true by definition or by calibrating a fitted value. The coverage comparison against STL, SSTL, and STREL is a human coding study of an external corpus of 1,000 requirements, not a derivation from SaSTL's own semantics, so any bias in the coding rules is an empirical validity risk, not a circular one. The New York City evaluation reuses the authors' own conflict-resolution framework [28], but only as evaluation infrastructure for the case study, and the formal soundness and monitoring results do not load-bearingly depend on that citation. No step in the paper equates an input with the output it is said to predict, renames a known result as new, or imports a uniqueness conclusion from same-author prior work as an external fact.

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

No fitted numerical parameters are introduced; the contribution is a formal logic plus an empirical evaluation. The main unproved inputs are the STL background, a fixed-graph spatial model, and an unpublished requirement corpus with self-coded labels.

assumptions (4)

standard math STL semantics and STL monitoring complexity are assumed as given from the cited literature.
SaSTL is defined as an extension of STL, and the temporal fragment correctness relies on STL results. Invoked in Section IV-A.
domain assumption The city is represented as a finite weighted undirected graph with fixed node positions, so distances can be precomputed and queried with range trees.
Section IV-A and Lemma 1 assume a fixed grid and precomputed range trees; mobile sensors or dynamic topology are out of scope.
ad hoc to paper The 1,000 city requirements were collected and labeled by graduate students as quantitatively specified and as expressible or not expressible in each logic.
Section III and Section VI-C; the coverage comparison depends entirely on this unpublished annotation process.
domain assumption Sensor data streams are synchronized over time and locations, and signals are comparable across locations for sum and average aggregation.
The aggregation operators average or sum over locations in alpha_x, which requires aligned sampling and consistent units. This is assumed in the semantics and algorithms.

how reviews work

0 comments

Cite this review

Pith. "Pith review of SaSTL: Spatial Aggregation Signal Temporal Logic for Runtime Monitoring in Smart Cities." pith.science (2026). https://pith.science/paper/5QULETAK

@misc{pith2026190802366,
  author       = {Pith},
  title        = {Pith review of: SaSTL: Spatial Aggregation Signal Temporal Logic for Runtime Monitoring in Smart Cities},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5QULETAK}},
  note         = {Machine review of arXiv:1908.02366}
}

read the original abstract

We present SaSTL -- a novel Spatial Aggregation Signal Temporal Logic -- for the efficient runtime monitoring of safety and performance requirements in smart cities. We first describe a study of over 1,000 smart city requirements, some of which can not be specified using existing logic such as Signal Temporal Logic (STL) and its variants. To tackle this limitation, we develop two new logical operators in SaSTL to augment STL for expressing spatial aggregation and spatial counting characteristics that are commonly found in real city requirements. We also develop efficient monitoring algorithms that can check a SaSTL requirement in parallel over multiple data streams (e.g., generated by multiple sensors distributed spatially in a city). We evaluate our SaSTL monitor by applying to two case studies with large-scale real city sensing data (e.g., up to 10,000 sensors in one requirement). The results show that SaSTL has a much higher coverage expressiveness than other spatial-temporal logics, and with a significant reduction of computation time for monitoring requirements. We also demonstrate that the SaSTL monitor can help improve the safety and performance of smart cities via simulated experiments.

Figures

Figures reproduced from arXiv: 1908.02366 by the authors.

**Figure 2.** An example of city abstracted graph. A require [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

**Figure 3.** Partial Maps of Chicago and New York with [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

Figures from the paper (3 more)

**Figure 4.** Figure 4: Requirement Satisfaction Rate during Different [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]

**Figure 7.** Figure 7: Comparison of the Specification Coverage on 1000 [PITH_FULL_IMAGE:figures/full_fig_p010_7.png]

**Figure 6.** Figure 6: Distributions of the violations over requirements [PITH_FULL_IMAGE:figures/full_fig_p010_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

41 extracted references · 41 canonical work pages

[1]

Array of things: a scientiﬁc research instrument in the public way: platform design and early lessons learned,

C. E. Catlett, P. H. Beckman, R. Sankaran, and K. K. Galvin, “Array of things: a scientiﬁc research instrument in the public way: platform design and early lessons learned,” in Proceedings of the 2nd International Workshop on Science of Smart City Operations and Platforms Engineering . ACM, 2017, pp. 26–33

work page 2017
[2]

IBM takes ‘smarter cities’ to rio de janeiro,

New York Times, “IBM takes ‘smarter cities’ to rio de janeiro,” 2012

work page 2012
[3]

Smart+connected operations center,

Cisco, “Smart+connected operations center,” 2017

work page 2017
[4]

Data sets, modeling, and decision making in smart cities: A survey,

M. Ma, S. M. Preum, M. Y . Ahmed, W. Tärneberg, A. Hen- dawi, and J. A. Stankovic, “Data sets, modeling, and decision making in smart cities: A survey,” ACM Transactions on Cyber-Physical Systems, vol. 4, no. 2, pp. 1–28, 2019

work page 2019
[5]

Dynamic integration of heterogeneous trans- portation modes under disruptive events,

Y . Yuan, D. Zhang, F. Miao, J. A. Stankovic, T. He, G. Pappas, and S. Lin, “Dynamic integration of heterogeneous trans- portation modes under disruptive events,” in 2018 ACM/IEEE 9th International Conference on Cyber-Physical Systems (IC- CPS). IEEE, 2018, pp. 65–76

work page 2018
[6]

Cityguard: A watchdog for safety-aware conﬂict detection in smart cities,

M. Ma, S. M. Preum, and J. A. Stankovic, “Cityguard: A watchdog for safety-aware conﬂict detection in smart cities,” in Proceedings of the Second International Conference on Internet-of-Things Design and Implementation , 2017, pp. 259–270

work page 2017
[7]

Detecting urban anomalies using multiple spatio-temporal data sources,

H. Zhang, Y . Zheng, and Y . Yu, “Detecting urban anomalies using multiple spatio-temporal data sources,” ACM on Inter- active, Mobile, Wearable and Ubiquitous Technologies, vol. 2, no. 1, p. 54, 2018

work page 2018
[8]

A case study of trust on autonomous driving,

S. Sheng, E. Pakdamanian, K. Han, B. Kim, P. Tiwari, I. Kim, and L. Feng, “A case study of trust on autonomous driving,” in 2019 IEEE Intelligent Transportation Systems Conference (ITSC). IEEE, 2019, pp. 4368–4373

work page 2019

Show all 41 references

[9]

Runtime monitoring of safety and performance requirements in smart cities,

M. Ma, J. A. Stankovic, and L. Feng, “Runtime monitoring of safety and performance requirements in smart cities,” in 1st ACM Workshop on the Internet of Safe Things , 2017

2017
[10]

Spatel: a novel spatial-temporal logic and its ap- plications to networked systems,

I. Haghighi, A. Jones, Z. Kong, E. Bartocci, R. Gros, and C. Belta, “Spatel: a novel spatial-temporal logic and its ap- plications to networked systems,” in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM, 2015, pp. 189–198

2015
[11]

Cityresolver: a decision support system for conﬂict resolution in smart cities,

M. Ma, J. A. Stankovic, and L. Feng, “Cityresolver: a decision support system for conﬂict resolution in smart cities,” in Proceedings of the 9th ACM/IEEE International Conference on Cyber-Physical Systems . IEEE Press, 2018, pp. 55–64

2018
[12]

Monitoring temporal properties of continuous signals,

O. Maler and D. Nickovic, “Monitoring temporal properties of continuous signals,” in Proc. FORMATS, 2004

2004
[13]

Qualitative and quantitative monitoring of spatio-temporal properties,

L. Nenzi, L. Bortolussi, V . Ciancia, M. Loreti, and M. Massink, “Qualitative and quantitative monitoring of spatio-temporal properties,” in Runtime Veriﬁcation - 6th International Conference, RV 2015 , vol. 9333. Springer, 2015, pp. 21–37

2015
[14]

Monitor- ing mobile and spatially distributed cyber-physical systems,

E. Bartocci, L. Bortolussi, M. Loreti, and L. Nenzi, “Monitor- ing mobile and spatially distributed cyber-physical systems,” in MEMOCODE 2017: the 15th ACM-IEEE International Conference on Formal Methods and Models for System De- sign. ACM, 2017, pp. 146–155

2017
[15]

Emissions from transportation, nyc environment protection,

NYC.gov, “Emissions from transportation, nyc environment protection,” 2019. [Online]. Available: https://www1.nyc.gov/ html/dep/html/air/emissions_from_transportation.shtml

2019
[16]

Air quality - motor vehicular pollutants, lead, odors, and nuisance pollutants,

District of Columbia Municipal Regulations and D. of Columbia Register, “Air quality - motor vehicular pollutants, lead, odors, and nuisance pollutants,” 2016

2016
[17]

A local law to amend the admin- istrative code of the city of new york, in relation to restricting the use of bus lanes by sight-seeing buses,

S. Matteo and J. Brannan, “A local law to amend the admin- istrative code of the city of new york, in relation to restricting the use of bus lanes by sight-seeing buses,” in Restricting the use of bus lanes by sight-seeing buses . The New York City Council, 2019

2019
[18]

Use of heating oil remaining in tanks

NYC Environment Protection, “Use of heating oil remaining in tanks.” The city of New York, 2019

2019
[19]

Residential energy efﬁciency,

United States Environmental Protection Agency, “Residential energy efﬁciency,” in Energy Resources for State and Local Governments. The city of New York, 2019

2019
[20]

Ofﬁcial city of los angeles municipal code,

LA Sec 111.03. Minimum Ambient Noise Level, “Ofﬁcial city of los angeles municipal code,” 2016

2016
[21]

Guide to indoor air quality management in hong kong regional ofﬁces and public places,

Hong Kong, “Guide to indoor air quality management in hong kong regional ofﬁces and public places,” in Guide to Indoor Air Quality Management , 2019

2019
[22]

Stopping, standing or parking prohibited in spec- iﬁed places,

NYC.gov, “Stopping, standing or parking prohibited in spec- iﬁed places,” in New York Public Law , 2016

2016
[23]

Pre-hospital medical emergency regulations,

Beijing Emergency Agency, “Pre-hospital medical emergency regulations,” 2016

2016
[24]

Safety management for kindergarten, primary and secondary school,

Beijing Government, “Safety management for kindergarten, primary and secondary school,” 2016

2016
[25]

Efﬁcient robust mon- itoring for STL,

A. Donzé, T. Ferrere, and O. Maler, “Efﬁcient robust mon- itoring for STL,” in International Conference on Computer Aided Veriﬁcation. Springer, 2013, pp. 264–279

2013
[26]

A data structure for orthogonal range queries,

G. S. Lueker, “A data structure for orthogonal range queries,” in 19th Annual Symposium on Foundations of Computer Science. IEEE Computer Society, 1978, pp. 28–34

1978
[27]

Crimes of Chicago - one year prior to present,

City of Chicago, “Crimes of Chicago - one year prior to present,” 2018

2018
[28]

Detection of runtime conﬂicts among ser- vices in smart cities,

M. Ma, S. M. Preum, W. Tarneberg, M. Ahmed, M. Ruiters, and J. Stankovic, “Detection of runtime conﬂicts among ser- vices in smart cities,” in 2016 IEEE International Conference on Smart Computing (SMARTCOMP) . IEEE, 2016, pp. 1– 10

2016
[29]

Sumo–simulation of urban mobility: an overview,

M. Behrisch, L. Bieker, J. Erdmann, and D. Krajzewicz, “Sumo–simulation of urban mobility: an overview,” in Pro- ceedings of SIMUL 2011 . ThinkMind, 2011

2011
[30]

socrata.com/

NYC.gov, New York City Open Data , https://nycopendata. socrata.com/
[31]

Cyber-physical systems and events,

C. L. Talcott, “Cyber-physical systems and events,” in Software-Intensive Systems and New Computing Paradigms - Challenges and Visions , ser. LNCS. Springer, 2008, vol. 5380, pp. 101–115

2008
[32]

Spatio-temporal event model for cyber-physical systems,

Y . Tan, M. C. Vuran, and S. Goddard, “Spatio-temporal event model for cyber-physical systems,” in 2009 29th IEEE International Conference on Distributed Computing Systems Workshops. IEEE, 2009, pp. 44–50

2009
[33]

Spatial logic and spatial model checking for closure spaces,

V . Ciancia, D. Latella, M. Loreti, and M. Massink, “Spatial logic and spatial model checking for closure spaces,” in Proc. of SFM 2016 , ser. LNCS, vol. 9700. Springer, 2016, pp. 156–201

2016
[34]

SpaTeL: A Novel Spatial-Temporal Logic and Its Applications to Networked Systems,

I. Haghighi, A. Jones, J. Z. Kong, E. Bartocci, G. R., and C. Belta, “SpaTeL: A Novel Spatial-Temporal Logic and Its Applications to Networked Systems,” inProc. of HSCC, 2015

2015
[35]

A formal methods approach to pattern synthesis in reaction diffusion systems,

E. A. Gol, E. Bartocci, and C. Belta, “A formal methods approach to pattern synthesis in reaction diffusion systems,” in Proc. of CDC , 2014

2014
[36]

Learning and detecting emergent behavior in networks of cardiac myocytes,

R. Grosu, S. A. Smolka, F. Corradini, A. Wasilewska, E. Entcheva, and E. Bartocci, “Learning and detecting emergent behavior in networks of cardiac myocytes,” Commun. ACM, vol. 52, no. 3, pp. 97–105, 2009. [Online]. Available: http://doi.acm.org/10.1145/1467247.1467271

2009
[37]

A spatial logic for concurrency (part i),

L. Caires and L. Cardelli, “A spatial logic for concurrency (part i),” Information and Computation , vol. 186, no. 2, pp. 194 – 235, 2003

2003
[38]

Multi-dimensional modal logic as a framework for spatio- temporal reasoning,

B. Bennett, A. G. Cohn, F. Wolter, and M. Zakharyaschev, “Multi-dimensional modal logic as a framework for spatio- temporal reasoning,” Applied Intelligence, vol. 17, no. 3, pp. 239–251, Sep. 2002

2002
[39]

A decidable spatial generalization of metric interval temporal logic,

D. Bresolin, P. Sala, D. D. Monica, A. Montanari, and G. Sci- avicco, “A decidable spatial generalization of metric interval temporal logic,” in 2010 17th International Symposium on Temporal Representation and Reasoning , 2010, pp. 95–102

2010
[40]

Undecidability of compass logic,

M. Marx and M. Reynolds, “Undecidability of compass logic,” J Logic Computation, vol. 9, no. 6, pp. 897–914, 1999

1999
[41]

Team-level programming of drone sensor networks,

L. Mottola, M. Moretta, K. Whitehouse, and C. Ghezzi, “Team-level programming of drone sensor networks,” in Proceedings of the 12th ACM Conference on Embedded Network Sensor Systems, SenSys ’14, Memphis, Tennessee, USA, November 3-6, 2014 . ACM, 2014, pp. 177–190

2014

Pith tools

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

[1] [1]

Array of things: a scientiﬁc research instrument in the public way: platform design and early lessons learned,

C. E. Catlett, P. H. Beckman, R. Sankaran, and K. K. Galvin, “Array of things: a scientiﬁc research instrument in the public way: platform design and early lessons learned,” in Proceedings of the 2nd International Workshop on Science of Smart City Operations and Platforms Engineering . ACM, 2017, pp. 26–33

work page 2017

[2] [2]

IBM takes ‘smarter cities’ to rio de janeiro,

New York Times, “IBM takes ‘smarter cities’ to rio de janeiro,” 2012

work page 2012

[3] [3]

Smart+connected operations center,

Cisco, “Smart+connected operations center,” 2017

work page 2017

[4] [4]

Data sets, modeling, and decision making in smart cities: A survey,

M. Ma, S. M. Preum, M. Y . Ahmed, W. Tärneberg, A. Hen- dawi, and J. A. Stankovic, “Data sets, modeling, and decision making in smart cities: A survey,” ACM Transactions on Cyber-Physical Systems, vol. 4, no. 2, pp. 1–28, 2019

work page 2019

[5] [5]

Dynamic integration of heterogeneous trans- portation modes under disruptive events,

Y . Yuan, D. Zhang, F. Miao, J. A. Stankovic, T. He, G. Pappas, and S. Lin, “Dynamic integration of heterogeneous trans- portation modes under disruptive events,” in 2018 ACM/IEEE 9th International Conference on Cyber-Physical Systems (IC- CPS). IEEE, 2018, pp. 65–76

work page 2018

[6] [6]

Cityguard: A watchdog for safety-aware conﬂict detection in smart cities,

M. Ma, S. M. Preum, and J. A. Stankovic, “Cityguard: A watchdog for safety-aware conﬂict detection in smart cities,” in Proceedings of the Second International Conference on Internet-of-Things Design and Implementation , 2017, pp. 259–270

work page 2017

[7] [7]

Detecting urban anomalies using multiple spatio-temporal data sources,

H. Zhang, Y . Zheng, and Y . Yu, “Detecting urban anomalies using multiple spatio-temporal data sources,” ACM on Inter- active, Mobile, Wearable and Ubiquitous Technologies, vol. 2, no. 1, p. 54, 2018

work page 2018

[8] [8]

A case study of trust on autonomous driving,

S. Sheng, E. Pakdamanian, K. Han, B. Kim, P. Tiwari, I. Kim, and L. Feng, “A case study of trust on autonomous driving,” in 2019 IEEE Intelligent Transportation Systems Conference (ITSC). IEEE, 2019, pp. 4368–4373

work page 2019