@book(Bel57, author = {R. E. Bellman}, year = {1957}, title = {Dynamic Programming}, publisher = {Princeton Univ. Press}, ) @inproceedings(BKKW15, author = {Roderick Bloem and Bettina K{\"o}nighofer and Robert K{\"o}nighofer and Chao Wang}, year = {2015}, title = {Shield Synthesis: - Runtime Enforcement for Reactive Systems}, editor = {Christel Baier}, booktitle = {TACAS}, series = {LNCS}, volume = {9035}, publisher = {Springer}, pages = {533--548}, doi = {10.1007/978-3-662-46681-0_51}, ) @inproceedings(CP03, author = {Gaurav Chakravorty and Paritosh K. Pandya}, year = {2003}, title = {Digitizing Interval Duration Logic}, editor = {Warren A. Hunt and Fabio Somenzi}, booktitle = {{CAV}}, series = {LNCS}, volume = {2725}, publisher = {Springer}, pages = {167--179}, doi = {10.1007/978-3-540-45069-6\_17}, ) @book(ZH04, author = {Zhou Chaochen and Michael R. Hansen}, year = {2004}, title = {Duration Calculus - {A} Formal Approach to Real-Time Systems}, series = {Monographs in Theoretical Computer Science. An {EATCS} Series}, publisher = {Springer}, doi = {10.1007/978-3-662-06784-0}, ) @article(CHR91, author = {Zhou Chaochen and C. A. R. Hoare and A. P. Ravn}, year = {1991}, title = {A Calculus of Durations}, journal = {Inf. Process. Lett.}, volume = {40}, number = {5}, pages = {269--276}, doi = {10.1016/0020-0190(91)90122-X}, ) @inproceedings(ET14, author = {R\"{u}diger Ehlers and Ufuk Topcu}, year = {2014}, title = {Resilience to Intermittent Assumption Violations in Reactive Synthesis}, booktitle = {HSCC}, series = {HSCC '14}, publisher = {ACM}, address = {New York, NY, USA}, pages = {203--212}, doi = {10.1145/2562059.2562128}, ) @article(KZHHJ11, author = {J. Katoen and I. S. Zapreev and E. M. Hahn and H. Hermanns and D. N. Jansen}, year = {2011}, title = {The ins and outs of the probabilistic model checker MRMC}, journal = {Performance Evaluation}, volume = {68}, pages = {89--220}, doi = {10.1016/j.peva.2010.04.001}, url = {http://www.sciencedirect.com/science/article/pii/S0166531610000660}, ) @article(Mon02, author = {N. Klarlund and M\o{}ller, A. and M. I. Schwartzbach}, year = {2001}, title = {{MONA} Implementation Secrets}, volume = {2088}, pages = {182--194}, doi = {10.1007/3-540-44674-5_15}, ) @article(KABHKTW17, author = {Bettina K{\"o}nighofer and Mohammed Alshiekh and Roderick Bloem and Laura Humphrey and Robert K{\"o}nighofer and Ufuk Topcu and Chao Wang}, year = {2017}, title = {Shield synthesis}, journal = {FMSD}, volume = {51}, number = {2}, pages = {332--361}, doi = {10.1007/s10703-017-0276-9}, ) @inproceedings(SP05, author = {Shankara Narayanan Krishna and Paritosh K. Pandya}, year = {2005}, title = {Modal Strength Reduction in Quantified Discrete Duration Calculus}, booktitle = {{FSTTCS}}, series = {LNCS}, volume = {3821}, publisher = {Springer}, pages = {444--456}, doi = {10.1007/11590156\_36}, ) @inproceedings(MPW17, author = {Raj Mohan Matteplackel and Paritosh K. Pandya and Amol Wakankar}, year = {2017}, title = {Formalizing Timing Diagram Requirements in Discrete Duration Calculus}, booktitle = {SEFM 2017}, series = {LNCS}, volume = {10469}, publisher = {Springer International Publishing}, pages = {253--268}, doi = {10.1007/978-3-319-66197-1_16}, ) @inproceedings(Pan01b, author = {Paritosh K. Pandya}, year = {2001}, title = {Model Checking {CTL}*[{DC}]}, booktitle = {TACAS}, series = {LNCS}, volume = {2031}, publisher = {Springer}, pages = {559--573}, doi = {10.1007/3-540-45319-9_38}, ) @inproceedings(Pan01a, author = {Paritosh K. Pandya}, year = {2001}, title = {Specifying and deciding quantified discrete-time duration calculus formulae using DCVALID}, booktitle = {RTTOOLS (affiliated with CONCUR 2001)}, publisher = {CiteSeer}, ) @article(Pan05, author = {Paritosh K. Pandya}, year = {2005}, title = {Finding Extremal Models of Discrete Duration Calculus formulae using Symbolic Search}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {128}, number = {6}, pages = {247 -- 262}, doi = {10.1016/j.entcs.2005.04.015}, url = {http://www.sciencedirect.com/science/article/pii/S1571066105002471}, note = {AVoCS 2004}, ) @article(PW19a, author = {Paritosh K. Pandya and Amol Wakankar}, year = {2019}, title = {Specification and Reactive Synthesis of Robust Controllers}, journal = {CoRR}, volume = {abs/1905.11157}, url = {http://arxiv.org/abs/1905.11157}, ) @book(Put94, author = {Martin L. Puterman}, year = {1994}, title = {Markov Decision Processes: Discrete Stochastic Dynamic Programming}, edition = {1st}, publisher = {John Wiley \& Sons, Inc.}, address = {New York, NY, USA}, doi = {10.1002/9780470316887}, ) @inproceedings(SPC05, author = {Babita Sharma and Paritosh K. Pandya and Supratik Chakraborty}, year = {2005}, title = {Bounded Validity Checking of Interval Duration Logic}, booktitle = {{TACAS}}, series = {LNCS}, volume = {3440}, publisher = {Springer}, pages = {301--316}, doi = {10.1007/978-3-540-31980-1\_20}, ) @article(WPM19, author = {Amol Wakankar and Paritosh K. Pandya and Raj Mohan Matteplackel}, year = {2019}, title = {{DCSYNTH:} {A} Tool for Guided Reactive Synthesis with Soft Requirements, (To Appear in Proc. VSTTE 2019)}, journal = {CoRR}, volume = {abs/1903.03991}, url = {http://arxiv.org/abs/1903.03991}, ) @article(Wu16a, author = {Meng Wu}, year = {2016}, title = {iShield2 Synthesizer}, journal = {https://bitbucket.org/mengwu/shield-synthesis/}, url = {https://bitbucket.org/mengwu/shield-synthesis/}, ) @inproceedings(WWZ17, author = {Meng {Wu} and H. {Zeng} and C. {Wang} and H. {Yu}}, year = {2017}, title = {INVITED: Safety guard: Runtime enforcement for safety-critical cyber-physical systems}, booktitle = {DAC}, publisher = {ACM}, pages = {1--6}, doi = {10.1145/3061639.3072957}, ) @inproceedings(WWZ16, author = {Meng Wu and Haibo Zeng and Chao Wang}, year = {2016}, title = {Synthesizing Runtime Enforcer of Safety Properties Under Burst Error}, editor = {Sanjai Rayadurgam and Oksana Tkachuk}, booktitle = {{NFM}}, series = {LNCS}, volume = {9690}, publisher = {Springer}, pages = {65--81}, doi = {10.1007/978-3-319-40648-0_6}, )