Temporal Behavior Trees: Robustness and Segmentation
Authors: 
Sebastian Schirmer, Jasdeep Singh, 
Emily Jensen, Johann Dauer, Bernd Finkbeiner, Sriram SankaranarayananAuthors Info & Claims
Article No.: 9, Pages 1 - 14
Abstract
This paper presents temporal behavior trees (TBT), a specification formalism inspired by behavior trees that are commonly used to program robotic applications. We then introduce the concept of trace segmentation, wherein given a TBT specification and a trace, we split the trace optimally into sub-traces that are associated with various portions of the TBT specification. Segmentation of a trace then serves to explain precisely how a trace satisfies or violates a specification, and which portions of a specification are actually violated. We introduce the syntax and semantics of TBT and compare their expressiveness in relation to temporal logic. Next, we define robustness semantics for TBT specification with respect to a trace. Rather than a Boolean interpretation, the robustness provides a real-valued numerical outcome that quantifies how close or far away a trace is from satisfying or violating a TBT specification. We show that computing the robustness of a trace also segments it into subtraces.Finally, we provide efficient approximations for computing robustness and segmentation for long traces with guarantees on the result.We demonstrate how segmentations are useful through applications such as understanding how novice users pilot an aerial vehicle through a sequence of waypoints in desktop experiments and the offline monitoring of automated lander for a drone on a ship. Our case studies demonstrate how TBT specification and segmentation can be used to understand and interpret complex behaviors of humans and automation in cyber-physical systems.
References
[1]
Rahib H. Abiyev, Nurullah Akkaya, and Ersin Aytac. 2013. Control of soccer robots using behaviour trees. In 9th Asian Control Conference, ASCC 2013, Istanbul, Turkey, June 23-26, 2013. IEEE, 1–6. https://doi.org/10.1109/ASCC.2013.6606326
[2]
Ezio Bartocci, Jyotirmoy Deshmukh, Alexandre Donzé, Georgios Fainekos, Oded Maler, Dejan Ničković, and Sriram Sankaranarayanan. 2018. Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. Lectures on Runtime Verification: Introductory and Advanced Topics (2018), 135–175.
[3]
Andreas Bauer, Martin Leucker, and Christian Schallhart. 2007. The good, the bad, and the ugly, but how ugly is ugly?. In International Workshop on Runtime Verification. Springer, 126–138.
[4]
Andreas Bauer, Martin Leucker, and Christian Schallhart. 2011. Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM) 20, 4 (2011), 1–64.
[5]
Johan Van Benthem. 2010. Modal Logic for Open Minds (Lecture Notes). CSLI Publications (Stanford University).
[6]
Sooyung Byeon, Joonwon Choi, Yutong Zhang, and Inseok Hwang. 2023. Stochastic-Skill-Level-Based Shared Control for Human Training in Urban Air Mobility Scenario. J. Hum.-Robot Interact. (jun 2023). https://doi.org/10.1145/3603194 Just Accepted.
[7]
Antonio Cau, Ben Moszkowski, and Hussein Zedan. 2006. Interval temporal logic. URL: http://www. cms. dmu. ac. uk/ cau/itlhomepage/itlhomepage. html (2006).
[8]
Yuxiao Chen, James Anderson, Karanjit Kalsi, Aaron D. Ames, and Steven H. Low. 2021. Safety-Critical Control Synthesis for Network Systems With Control Barrier Functions and Assume-Guarantee Contracts. IEEE Transactions on Control of Network Systems 8, 1 (2021), 487–499. https://doi.org/10.1109/TCNS.2020.3029183
[9]
Michele Colledanchise and Petter Ögren. 2018. Behavior trees in robotics and AI: An introduction. CRC Press.
[10]
Giuseppe De Giacomo and Moshe Y. Vardi. 2013. Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (Beijing, China) (IJCAI ’13). AAAI Press, 854–860.
[11]
Jyotirmoy V Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, and Sanjit A Seshia. 2017. Robust online monitoring of signal temporal logic. Formal Methods in System Design 51 (2017), 5–30.
[12]
Alexandre Donzé and Oded Maler. 2010. Robust satisfaction of temporal logic over real-valued signals. In International Conference on Formal Modeling and Analysis of Timed Systems. Springer, 92–106.
[13]
Georgios E Fainekos and George J Pappas. 2006. Robustness of temporal logic specifications. In International Workshop on Formal Approaches to Software Testing. Springer, 178–192.
[14]
Bernd Finkbeiner and Henny Sipma. 2004. Checking finite traces using alternating automata. Formal Methods in System Design 24 (2004), 101–127.
[15]
Razan Ghzouli, Thorsten Berger, Einar Broch Johnsen, Swaib Dragule, and Andrzej Wąsowski. 2020. Behavior Trees in Action: A Study of Robotics Applications. In Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering (Virtual, USA) (SLE 2020). Association for Computing Machinery, New York, NY, USA, 196–209. https://doi.org/10.1145/3426425.3426942
[16]
Joseph Halpern, Zohar Manna, and Ben Moszkowski. 1983. A hardware semantics based on temporal intervals. In Automata, Languages and Programming, Josep Diaz (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 278–291.
[17]
D. Harel and D. Peleg. 1985. Process logic with regular formulas. Theoretical Computer Science 38 (1985). https://doi.org/10.1016/0304-3975(85)90225-7
[18]
Jie He, Ezio Bartocci, Dejan Ničković, Haris Isakovic, and Radu Grosu. 2022. DeepSTL: From English Requirements to Signal Temporal Logic. In Proceedings of the 44th International Conference on Software Engineering (Pittsburgh, Pennsylvania) (ICSE ’22). Association for Computing Machinery, New York, NY, USA, 610–622. https://doi.org/10.1145/3510003.3510171
[19]
Keliang He, Morteza Lahijanian, Lydia E. Kavraki, and Moshe Y. Vardi. 2015. Towards manipulation planning with temporal logic specifications. In IEEE International Conference on Robotics and Automation, ICRA 2015, Seattle, WA, USA, 26-30 May, 2015. IEEE, 346–352. https://doi.org/10.1109/ICRA.2015.7139022
[20]
Zhuochao He, Xuyang Zhang, Simon Jones, Sabine Hauert, Dandan Zhang, and Nathan F. Lepora. 2023. TacMMs: Tactile Mobile Manipulators for Warehouse Automation. IEEE Robotics and Automation Letters 8, 8 (2023), 4729–4736. https://doi.org/10.1109/LRA.2023.3287363
[21]
Danying Hu, Yuanzheng Gong, Blake Hannaford, and Eric J Seibel. 2015. Semi-autonomous simulated brain tumor ablation with Raven II surgical robot using behavior trees. In 2015 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 3868–3875.
[22]
Hao Hu, Xiaoliang Jia, Kuo Liu, and Bingyang Sun. 2021. Self-Adaptive Traffic Control Model With Behavior Trees and Reinforcement Learning for AGV in Industry 4.0. IEEE Transactions on Industrial Informatics 17, 12 (2021), 7968–7979. https://doi.org/10.1109/TII.2021.3059676
[23]
Matteo Iovino, Edvards Scukins, Jonathan Styrud, Petter Ögren, and Christian Smith. 2022. A survey of behavior trees in robotics and ai. Robotics and Autonomous Systems 154 (2022), 104096.
[24]
Anja Johansson and Pierangelo Dell’Acqua. 2012. Emotional behavior trees. In 2012 IEEE Conference on Computational Intelligence and Games (CIG). IEEE, 355–362.
[25]
Hadas Kress-Gazit, Georgios E. Fainekos, and George J. Pappas. 2009. Temporal-Logic-Based Reactive Mission and Motion Planning. IEEE Transactions on Robotics 25, 6 (2009), 1370–1381. https://doi.org/10.1109/TRO.2009.2030225
[26]
Orna Kupferman, Giuseppe Perelli, and Moshe Y Vardi. 2016. Synthesis with rational environments. Annals of Mathematics and Artificial Intelligence 78, 1 (2016), 3–20.
[27]
Martin Leucker and César Sánchez. 2007. Regular linear temporal logic. In International colloquium on theoretical aspects of computing. Springer, 291–305.
[28]
Christopher D Marlin. 1979. Coroutines: A Programming Methodology, a Language Design, and an Implementation. Ph. D. Dissertation. University of Adelaide, Department of Computing Science.
[29]
M. Mateas and A. Stern. 2002. A behavior language for story-based believable agents. IEEE Intelligent Systems 17, 4 (2002), 39–47. https://doi.org/10.1109/MIS.2002.1024751
[30]
B. C. Moszkowski. 1998. Compositional Reasoning using Interval Temporal Logic and Tempura. In Compositionality: The Significant Difference, Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 439–464.
[31]
Ana Lúcia De Moura and Roberto Ierusalimschy. 2009. Revisiting Coroutines. ACM Trans. Program. Lang. Syst. 31, 2, Article 6 (feb 2009), 31 pages. https://doi.org/10.1145/1462166.1462167
[32]
Vasumathi Raman, Alexandre Donzé, Dorsa Sadigh, Richard M. Murray, and Sanjit A. Seshia. 2015. Reactive Synthesis from Signal Temporal Logic Specifications. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (Seattle, Washington) (HSCC ’15). Association for Computing Machinery, New York, NY, USA, 239–248. https://doi.org/10.1145/2728606.2728628
[33]
Aurélien Rizk, Grégory Batt, François Fages, and Sylvain Soliman. 2008. On a Continuous Degree of Satisfaction of Temporal Logic Formulae with Applications to Systems Biology. In Computational Methods in Systems Biology. Springer Berlin Heidelberg, 251–268.
[34]
Roni Rosner and Amir Pnueli. 1986. A Choppy Logic. In Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986) (Cambridge, MA, USA). IEEE Computer Society Press, 306–313.
[35]
Kirk Y. W. Scheper, Sjoerd Tijmons, Cornelis C. de Visser, and Guido C. H. E. de Croon. 2016. Behavior Trees for Evolutionary Robotics†. Artificial Life 22, 1 (02 2016), 23–48. https://doi.org/10.1162/ARTL_a_00192 arXiv:https://direct.mit.edu/artl/article-pdf/22/1/23/1665258/artl_a_00192.pdf
[36]
T. Schmelz and R. Lantzsch. 2018. Abschlussbericht: F&T Studie - Pilotenassistenz für Schiffsdecklandungen (PiloDeck)[Final report: F&T Study - Pilot assitance for ship deck landing (PiloDeck)],. Technical Note AHD-TN-ESPE-302-18 (2018).
[37]
Bianca Isabella Schuchardt, Thomas Dautermann, Alexander Donkels, Stefan Krause, Niklas Peinecke, and Gunnar Schwoch. 2020. Maritime operation of an unmanned rotorcraft with tethered ship deck landing system. CEAS Aeronautical Journal 12, 1 (9 2020), 1–9. https://elib.dlr.de/140951/
[38]
Aleksandr Sidorenko, Jesko Hermann, and Martin Ruskowski. 2022. Using Behavior Trees for Coordination of Skills in Modular Reconfigurable CPPMs. In 2022 IEEE 27th International Conference on Emerging Technologies and Factory Automation (ETFA). 1–8. https://doi.org/10.1109/ETFA52439.2022.9921558
[39]
Dogan Ulus, Thomas Ferrère, Eugene Asarin, and Oded Maler. 2014. Timed Pattern Matching. In Formal Modeling and Analysis of Timed Systems, Axel Legay and Marius Bozga (Eds.). Springer International Publishing, Cham, 222–236.
[40]
A. v. Perger, P. Gamper, and R. Witzmann. 2022. Behavior Trees for Smart Grid Control. IFAC-PapersOnLine 55, 9 (2022), 122–127. https://doi.org/10.1016/j.ifacol.2022.07.022 11th IFAC Symposium on Control of Power and Energy Systems CPES 2022.
[41]
Pierre Wolper. 1983. Temporal logic can be more expressive. Information and control 56, 1-2 (1983), 72–99.
Recommendations
Temporal Behavior Trees -- Segmentation
HSCC '24: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and ControlWe present our tool for the segmentation of temporal behavior trees (TBT), a novel formalism for monitoring specifications. TBTs can be easily retrofitted to behavior trees, commonly used to program robotic applications. Our tool supports the robustness ...
Automated MR Hip Bone Segmentation
DICTA '11: Proceedings of the 2011 International Conference on Digital Image Computing: Techniques and ApplicationsThe accurate segmentation of the bone and articular cartilages from magnetic resonance (MR) images of the hip is important for clinical studies and drug trials into conditions like osteoarthritis. In current studies, segmentations are obtained using ...
3D segmentation and labeling of fractured bone from CT images
The segmentation of fractured bone from computed tomographies (CT images) is an important process in medical visualization and simulation, because it enables such applications to use data of a specific patient. On the other hand, the labeling of ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 14 May 2024
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
HSCC '24
Sponsor:
Acceptance Rates
Overall Acceptance Rate 153 of 373 submissions, 41%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 361Total Downloads
- Downloads (Last 12 months)361
- Downloads (Last 6 weeks)96
Reflects downloads up to 12 Nov 2024
Other Metrics
Citations
Cited By
View allView Options
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML FormatGet Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in