×

Incremental reasoning in probabilistic signal temporal logic. (English) Zbl 1434.68562

Summary: Robot safety is of growing concern given recent developments in intelligent autonomous systems. For complex agents operating in uncertain, complex and rapidly-changing environments it is difficult to guarantee safety without imposing unrealistic assumptions and restrictions. It is therefore necessary to complement traditional formal verification with monitoring of the running system after deployment. Runtime verification can be used to monitor that an agent behaves according to a formal specification. The specification can contain safety-related requirements and assumptions about the environment, environment-agent interactions and agent-agent interactions. A key problem is the uncertain and changing nature of the environment. This necessitates requirements on how probable a certain outcome is and on predictions of future states. We propose Probabilistic Signal Temporal Logic (ProbSTL) by extending Signal Temporal Logic with a sub-language to allow statements over probabilities, observations and predictions. We further introduce and prove the correctness of the incremental stream reasoning technique progression over well-formed formulas in ProbSTL. Experimental evaluations demonstrate the applicability and benefits of ProbSTL for robot safety.

MSC:

68T30 Knowledge representation
03B44 Temporal logic
68T27 Logic in artificial intelligence
68T40 Artificial intelligence for robotics
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Dell’Aglio, D.; Della Valle, E.; van Harmelen, F.; Bernstein, A., Stream reasoning: a survey and outlook, Data Sci., 1, 59-83 (2017)
[2] Tiger, M.; Heintz, F., Stream reasoning using temporal logic and predictive probabilistic state models, (Proceedings of the 23rd International Symposium on Temporal Representation and Reasoning (TIME) (2016), IEEE), 196-205
[3] Alqahtani, S.; Taylor, S.; Riley, I.; Gamble, R.; Mailler, R., Predictive path planning algorithm using kalman filters and mtl robustness, (2018 IEEE International Symposium on Safety, Security, and Rescue Robotics (SSRR) (2018), IEEE), 1-7
[4] Bartocci, E.; Falcone, Y.; Francalanza, A.; Reger, G., Introduction to Runtime Verification, 1-33 (2018), Springer International Publishing: Springer International Publishing Cham
[5] Bartocci, E.; Deshmukh, J.; Donzé, A.; Fainekos, G.; Maler, O.; Ničković, D.; Sankaranarayanan, S., Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications, (Lectures on Runtime Verification (2018), Springer), 135-175
[6] Lamine, K. B.; Kabanza, F., Using fuzzy temporal logic for monitoring behavior-based mobile robots, (Proc. of Int. Conf. on Robotics and Applications (IASTED) (2000)), 116-121
[7] Pérez, J.; Jiménez, J.; Rabanal, A.; Astarloa, A.; Lázaro, J., Ftl-cfree: a fuzzy real-time language for runtime verification, IEEE Trans. Ind. Inform., 10, 3, 1670-1683 (2014)
[8] Schön, T.; Gustafsson, F.; Nordlund, P.-J., Marginalized particle filters for mixed linear/nonlinear state-space models, IEEE Trans. Signal Process., 53, 7, 2279-2289 (2005) · Zbl 1370.94229
[9] Fox, D.; Hightower, J.; Liao, L.; Schulz, D.; Borriello, G., Bayesian filtering for location estimation, IEEE Pervasive Comput., 3, 24-33 (2003)
[10] Nitti, D.; Laet, T. D.; Raedt, L. D., A particle filter for hybrid relational domains, (Proc. International Conference on Intelligent Robots and Systems (IROS) (2013))
[11] Kovtunova, A.; Penaloza, R., Cutting diamonds: a temporal logic with probabilistic distributions, (Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR) (2018))
[12] De Raedt, L.; Kimmig, A., Probabilistic (logic) programming concepts, Mach. Learn., 100, 1, 5-47 (2015) · Zbl 1346.68050
[13] Doherty, P.; Kvarnström, J.; Heintz, F., A temporal logic-based planning and execution monitoring framework for unmanned aircraft systems, Auton. Agents Multi-Agent Syst., 19, 3, 332-377 (2009)
[14] Koymans, R., Specifying real-time properties with metric temporal logic, Real-Time Syst., 2, 4, 255-299 (1990)
[15] Alur, R.; Feder, T.; Henzinger, T. A., The benefits of relaxing punctuality, J. ACM, 43, 1, 116-146 (1996) · Zbl 0882.68021
[16] Maler, O.; Nickovic, D., Monitoring temporal properties of continuous signals, (Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems (2004), Springer), 152-166 · Zbl 1109.68518
[17] Brim, L.; Dluhoš, P.; Šafránek, D.; Vejpustek, T., Stl⁎: extending signal temporal logic with signal-value freezing operator, Inf. Comput., 236, 52-67 (2014) · Zbl 1311.68085
[18] Yoo, C.; Belta, C., Rich time series classification using temporal logic, (Robotics: Science and Systems (RSS) (2017))
[19] Sadigh, D.; Kapoor, A., Safe control under uncertainty with probabilistic signal temporal logic, (Proceedings of Robotics: Science and Systems. Proceedings of Robotics: Science and Systems, AnnArbor, Michigan (2016))
[20] Bacchus, F.; Kabanza, F., Planning for temporally extended goals, Ann. Math. Artif. Intell., 22, 1-2, 5-27 (1998) · Zbl 1034.68549
[21] Markey, N.; Schnoebelen, P., Model checking a path, (International Conference on Concurrency Theory (2003), Springer), 251-265 · Zbl 1274.68197
[22] Basin, D.; Bhatt, B. N.; Traytel, D., Almost event-rate independent monitoring of metric temporal logic, (Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2017)), 94-112 · Zbl 1452.68278
[23] Serra, R.; Arzelier, D.; Joldes, M.; Lasserre, J.-B.; Rondepierre, A.; Salvy, B., Fast and accurate computation of orbital collision probability for short-term encounters, J. Guid. Control Dyn., 1009-1021 (2016)
[24] Santipantakis, G. M.; Vlachou, A.; Doulkeridis, C.; Artikis, A.; Kontopoulos, I.; Vouros, G. A., A stream reasoning system for maritime monitoring, (25th International Symposium on Temporal Representation and Reasoning (TIME) (2018))
[25] Novak, E., Some results on the complexity of numerical integration, (Springer Proceedings in Mathematics and Statistics, vol. 163 (2016)), 161-183 · Zbl 1356.65085
[26] Thrun, S., Particle filters in robotics, (Proceedings of the Eighteenth conference on Uncertainty in artificial intelligence (UAI) (2002), Morgan Kaufmann Publishers Inc.), 511-518
[27] Nyquist, H., Certain topics in telegraph transmission theory, Trans. Am. Inst. Electr. Eng., 47, 2, 617-644 (1928)
[28] Andersson, O.; Ljungqvist, O.; Tiger, M.; Axehill, D.; Heintz, F., Receding-horizon lattice-based motion planning with dynamic obstacle avoidance, (2018 IEEE Conference on Decision and Control (CDC) (2018)), 4467-4474
[29] Kamel, M.; Stastny, T.; Alexis, K.; Siegwart, R., Model predictive control for trajectory tracking of unmanned aerial vehicles using robot operating system, (Robot Operating System (ROS) (2017), Springer), 3-39
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.