Temporal Logic Monitoring Complexity

Results from [ThatiR05]
- Algorithm is referred to as resolving the past and deriving the future
  - involves transforming the formula
- Metric Temporal Logic with both Past and Future
- Upperbounds
  - MTL + Past + Future
    - Space: $O(m 2^m)$
    - Time: $O(m^3 2^{3m})$ for processing each event
    - $m$ is size of formula + sum of numercal constants
    - Doubly exponential in size of the formula if constants are in binary
  - LTL + Past Only
    - Space: $O(|\varphi|)$
    - Time: $O(|\varphi|)$ for processing each event
- Lowerbounds
  - MTL + Past + Future
    - There is at least one $\varphi$ such that monitoring requires space at least $\Omega(2^{\alpha c \sqrt{|\underline{\varphi}|}})$
      - $c$ is the largest constant occurring in $\varphi$
      - $\alpha$ is a fixed constant
      - $\underline{\varphi}$ is $\varphi$ without any numerical constants
    - There is at least one $\varphi$ such that monitoring requires space at least $\Omega(2^{2^{\alpha |\varphi|}})$
  - MTL + Future Only
    - Same results hold
  - LTL + Future + Past
    - There is a formula $\varphi$ such that monitoring requires space at least $\Omega(2^{\alpha \sqrt{|\varphi|}})$
Results from [MarkeyS03]
- LTL + Past can be solved in time $O(|w| \times |\varphi|)$
- The dynamic programming algorithm is attributed by [ThatiR05] to this paper
- There are additional results about
  - Model checking for infinite paths of the form $w_1 \cdot w_2^\omega$
  - LTL + Chop, LTL + Forgettable Past
  - Model Checking paths written using exponents
Results from [SenRA03]
- Monitoring Boolean LTL + Future Only + Infinite Traces
- Aim: To produce an automaton which can detect good and bad prefixes
  - Good Prefixes: all extensions are accepted
  - Bad Prefixes: no extensions are accepted
- Space Lowerbound
  - $\Omega(2^{2^{|\varphi|}})$ states
  - That is, $\Omega(2^{|\varphi|})$ bits
- Involves this language: ${ \sigma # w # \sigma' $ w \mid w \in {0, 1}^k \text{ and } \sigma, \sigma' \in {0, 1, #}^* }$
  - This can be encoded in a LTL formula of size $O(k^2)$
- This idea is also used in [KupfermaV2001], [KupfermaV1998] and the language was probably originally defined in [ChandraKS81]
Results from [MalerN2004]
- Boolean Metric STL + Continuous Signals + Future Time only
- Offline Monitoring
- Total time needed: $O(k \cdot n)$
  - $k$ is the number of sub-formulas
  - and $n$ is the number of positive intervals
Results from [DonzeFM2013]
- Robustness Metric STL + Continous Signals + Future Time only
- Offline Algorithm
- Time Complexity: $O(|\varphi| \cdot |w| \cdot d^{h(\varphi)})$
  - $h(\varphi)$ is the height of the formula
Results from [DokhanchiHF2014]
- Robustness Metric STL + Discrete Signals + Bounded Future + Unbounded Past + Online
- Space Complexity: Table for Robustness of Previous Values
- Time Complexity: Quadratic in the difference of History and Horizon
- [DeshmukhDGJ2017] may have improved on this
  - They use Lemire's sliding window maximum

@article{ThatiR05,
    author = {Prasanna Thati and Grigore Rosu},
    title = {Monitoring Algorithms for Metric Temporal Logic Specifications},
    journal = {Electronic Notes in Theoretical Computer Science},
    volume = {113},
    pages = {145-162},
    year = {2005},
    note = {Proceedings of the Fourth Workshop on Runtime Verification (RV 2004)},
    issn = {1571-0661},
    doi = {https://doi.org/10.1016/j.entcs.2004.01.029},
}

@inproceedings{MarkeyS03,
    author="Markey, N.
        and Schnoebelen, P.",
    editor="Amadio, Roberto
        and Lugiez, Denis",
    title="Model Checking a Path",
    booktitle="CONCUR 2003 - Concurrency Theory",
    year="2003",
    publisher="Springer Berlin Heidelberg",
    address="Berlin, Heidelberg",
    pages="251--265",
    isbn="978-3-540-45187-7"
}

@inproceedings{SenRA03,
    author="Sen, Koushik
        and Ro{\c{s}}u, Grigore
        and Agha, Gul",
    editor="Saraswat, Vijay A.",
    title="Generating Optimal Linear Temporal Logic Monitors by Coinduction",
    booktitle="Advances in Computing Science -- ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation",
    year="2003",
    publisher="Springer Berlin Heidelberg",
    address="Berlin, Heidelberg",
    pages="260--275",
    isbn="978-3-540-40965-6"
}

@article{KupfermaV2001,
    author = {Kupferman, Orna and Vardi, Moshe Y.},
    title = {Model Checking of Safety Properties},
    journal = {Formal Methods in System Design},
    year = {2001},
    volume = {19},
    number = {3},
    pages = {291--314},
    issn = {1572-8102},
    doi = {10.1023/A:1011254632723},
}

@inproceedings{KupfermanV1998,
  author={Kupferman, O. and Vardi, M.Y.},
  booktitle={Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.98CB36226)}, 
  title={Freedom, weakness, and determinism: from linear-time to branching-time}, 
  year={1998},
  volume={},
  number={},
  pages={81-92},
  doi={10.1109/LICS.1998.705645}
}

@article{ChandraKS81,
  title={Alternation},
  author={Chandra, Ashok K and Kozen, Dexter C and Stockmeyer, Larry J},
  journal={Journal of the ACM (JACM)},
  volume={28},
  number={1},
  pages={114--133},
  year={1981},
  publisher={ACM New York, NY, USA}
}

@inproceedings{DonzeFM2013,
    author="Donz{\'e}, Alexandre
        and Ferr{\`e}re, Thomas
        and Maler, Oded",
    editor="Sharygina, Natasha
        and Veith, Helmut",
    title="Efficient Robust Monitoring for STL",
    booktitle="Computer Aided Verification",
    year="2013",
    publisher="Springer Berlin Heidelberg",
    address="Berlin, Heidelberg",
    pages="264--279",
    isbn="978-3-642-39799-8"
}

@inproceedings{MalerN2004,
    author="Maler, Oded
        and Nickovic, Dejan",
    editor="Lakhnech, Yassine
        and Yovine, Sergio",
    title="Monitoring Temporal Properties of Continuous Signals",
    booktitle="Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems",
    year="2004",
    publisher="Springer Berlin Heidelberg",
    address="Berlin, Heidelberg",
    pages="152--166",
    isbn="978-3-540-30206-3"
}

@inproceedings{DokhanchiHF2014,
    author="Dokhanchi, Adel
        and Hoxha, Bardh
        and Fainekos, Georgios",
    editor="Bonakdarpour, Borzoo
        and Smolka, Scott A.",
    title="On-Line Monitoring for Temporal Logic Robustness",
    booktitle="Runtime Verification",
    year="2014",
    publisher="Springer International Publishing",
    address="Cham",
    pages="231--246",
    isbn="978-3-319-11164-3"
}

@article{DeshmukhDGJ2017,
    author = {Deshmukh, Jyotirmoy V. and Donzé, Alexandre and Ghosh, Shromona and Jin, Xiaoqing and Juniwal, Garvit and Seshia, Sanjit A.},
    title = {Robust online monitoring of signal temporal logic},
    journal = {Formal Methods in System Design},
    year = {2017},
    volume = {51},
    number = {1},
    pages = {5--30},
    issn = {1572-8102},
    doi = {10.1007/s10703-017-0286-7},
}

Agnishom/complexity.md