Abstract
The Multi-Lane Spatial Logic MLSL introduced by Hilscher et al. in [4] is a two-dimensional spatial logic geared towards modelling and analysis of traffic situations, where the two dimensions are interpreted as the lanes of a road and the distance travelled down that road, respectively. The intended use of MLSL is for capturing (and reasoning about) guards and invariants in decision-making schemes for highly automated driving [12]. Unfortunately, the logic turns out to be undecidable [7, 8, 11], rendering implementability and thus the actual use of such guard conditions in real-time decision making questionable in general.
We here show that under a reasonable model of technical observation of the traffic situation, the actual decidability and implementability issues take a much more pleasing form: given that an actual autonomous car can only sample state information of a finite set of environmental cars in real-time, we show that it is decidable whether truth of an arbitrary MLSL formula can be safely determined on a given sample size. For such feasible formulas, we furthermore state a procedure for determining their truth values based on such a sample.
M. Fränzle—Work of the author was partially supported by Deutsche Forschungsgemeinschaft within the Transregional Collaborative Research Center SFB/TR 14 AVACS.
M.R. Hansen—Work of the author was partially supported by the Danish Research Foundation for Basic Research within the IDEA4CPS project.
H. Ody—Work of the author was partially supported by Deutsche Forschungsgemeinschaft within the Research Training Group DFG GRK 1765 SCARE.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Allen, J.F.: Maintaining knowledge about temporal intervals. Communications of the ACM 26(11), 832–843 (1983)
Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. Journal of the ACM (JACM) 38(4), 935–962 (1991)
Hilscher, M., Linker, S., Olderog, E.-R., Ravn, A.P.: An Abstract Model for Proving Safety of Multi-lane Traffic Manoeuvres. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 404–419. Springer, Heidelberg (2011)
Hilscher, M., Linker, S., Olderog, E.-R.: Proving Safety of Traffic Manoeuvres on Country Roads. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 196–212. Springer, Heidelberg (2013)
Klebelsberg, D.: Verkehrspsychologie. Springer (2013)
Linker, S.: Proofs for traffic safety : combining diagrams and logic. Ph.D. thesis, Carl von Ossietzky University of Oldenburg (2015)
Linker, S., Hilscher, M.: Proof Theory of a Multi-Lane Spatial Logic. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 231–248. Springer, Heidelberg (2013)
Monniaux, D.: A Quantifier Elimination Algorithm for Linear Real Arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 243–257. Springer, Heidelberg (2008)
Moszkowski, B.: A temporal logic for multi-level reasoning about hardware. IEEE Computer 18(2), 10–19 (1985)
Ody, H.: Analysing decision problems of multi-lane spatial logic (2015) (manuscript). http://theoretica.informatik.uni-oldenburg.de/ sefie/files/decidability.pdf
Olderog, E.-R., Ravn, A.P., Wisniewski, R.: Linking Discrete and Continuous Models (2014) (manuscript)
Schäfer, A.: A Calculus for Shapes in Time and Space. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 463–477. Springer, Heidelberg (2005)
Venema, Y.: A modal logic for chopping intervals. Journal of Logic and Computation 1(4), 453–476 (1991)
Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: ISSAC, pp. 129–136. ACM (1999)
Woodcock, J., Davies, J.: Using Z – Specification, Refinement, and Proof. Prentice Hall (1996)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Fränzle, M., Hansen, M.R., Ody, H. (2015). No Need Knowing Numerous Neighbours. In: Meyer, R., Platzer, A., Wehrheim, H. (eds) Correct System Design. Lecture Notes in Computer Science(), vol 9360. Springer, Cham. https://doi.org/10.1007/978-3-319-23506-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-23506-6_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23505-9
Online ISBN: 978-3-319-23506-6
eBook Packages: Computer ScienceComputer Science (R0)