A4 – Logic-Based Perspicuous Run-Time Supervision

This project investigates perspicuous supervision of technical systems, carried out in a read data—analyse—react loop (RAR loop) several times per second. Our vision is a supervisor implemented by logical rules (clauses) out of a dedicated logical fragment, constituting a paradigm shift where (i) the declarative representation and formal logical reasoning provides explications, turning what is now a black box into a perspicuous system; (ii) testing can be replaced by automatic verification; (iii) the verified clauses can be deployed in a RAR loop; and as a consequence (iv) the overall product cycle is less costly. To these ends, we will investigate logical fragments combining (decidable) first-order logic fragments, representing control aspects, with (decidable) arithmetic theories, representing the abstraction of real-world technical system behaviour.

Principal Investigators

Principal Investigator
Max Planck Institute for Informatics
Principal Investigator
Technische Universität Dresden
Principal Investigator
Technische Universität Dresden

Researchers

Martin Bromberger
( )
Irina Dragoste
( , )
Rasha Faqeh
( , )
Maximilian Marx
( , )
Saidgani Musaev
( , )
Oleksii Oleksenko
( , )
Muhammad Usama Sardar
( , )
Uwe Waldmann
( )

Publications

View all Publications
Loading Data...