Monitoring of Spatio-Temporal Properties with Nonlinear SAT solvers

Matos Pedro, André; Silva, Tomás; Sequeira, Tiago; Lourenço, João; Seco, João Costa; Ferreira, Carla

http://hdl.handle.net/10362/170716

Utilize este identificador para referenciar este registo.

Nome:	Descrição:	Tamanho:	Formato:
Monitoring_of_spatio-temporal_properties_with_nonlinear.pdf		1.89 MB	Adobe PDF	Ver/Abrir

Contacte-nos

Autores

Resumo(s)

The automotive industry is increasingly dependent on computing systems with different critical requirements. The verification and validation methods for these systems are now leveraging complex AI methods, for which the decision algorithms introduce non-determinism, especially in autonomous driving. This paper presents a runtime verification technique agnostic to the target system, which focuses on monitoring spatio-temporal properties that abstract the evolution of objects’ behavior in their spatial and temporal flow. First, a formalization of three known traffic rules (from the Vienna convention on road traffic) is presented, where a spatio-temporal logic fragment is used. Then, these logical expressions are translated to a monitoring model written in first-order logic, where they are processed by a non-linear satisfiability solver. Finally, the translation allows the solver to check the validity of the encoded properties according to an instance of a specific traffic scenario (a trace). The results obtained from our tool, which automatically generates a monitor from a formula, show that our approach is feasible for online monitoring in a real-world environment.

Descrição

Funding Information: Open access funding provided by FCT|FCCN (b-on). This work is supported by the EU/Next Generation EU, through Programa de Recuperação e Resiliência (PRR) [Project Route 25 No. C645463824-00000063]. This work was also partially supported by: i) the European Regional Development Fund (ERDF) through the Competitiveness and Internationalization Operational Program (COMPETE 2020) of Portugal 2020 [Project STEROID with No. 069989 (POCI-01-0247-FEDER-069989)]. Publisher Copyright: © The Author(s) 2024.

Palavras-chave

Autonomous vehicles Formalization of traffic rules Non-linear SAT solvers Runtime verification Rutime monitoring Spatio-temporal logic Software Information Systems