Proving the consistency of Signal Temporal Logic Requirements
Presenter: Beatrice Melani
DEIB - Conference Room "E. Gatti" (Bld. 20)
March 18th, 2025 | 11.30 am
Contact: Prof. Simone Formentin
DEIB - Conference Room "E. Gatti" (Bld. 20)
March 18th, 2025 | 11.30 am
Contact: Prof. Simone Formentin
Sommario
On March 18th, 2025 at 11.30 am Beatrice Melani, PHD Student in Information Technology, will hold a seminar on "Proving the consistency of Signal Temporal Logic Requirements" at DEIB Conference Room "Emilio Gatti" (Building 20).
In the context of Systems Engineering, and more precisely in the Requirement Management Process, an important issue is how to automatically and efficiently validate whether a set of requirements is consistent. When requirements are written using a formal specification language, the problem amounts to solve a satisfiability problem. For this purpose, I am presenting a novel one-pass, tree-shaped tableau method to assess the satisfiability of discrete-time Signal Temporal Logic requirements. The method includes heuristics which reduce the depth of the tree and make the approach more efficient than SMT encoding of STL formulas.
In the context of Systems Engineering, and more precisely in the Requirement Management Process, an important issue is how to automatically and efficiently validate whether a set of requirements is consistent. When requirements are written using a formal specification language, the problem amounts to solve a satisfiability problem. For this purpose, I am presenting a novel one-pass, tree-shaped tableau method to assess the satisfiability of discrete-time Signal Temporal Logic requirements. The method includes heuristics which reduce the depth of the tree and make the approach more efficient than SMT encoding of STL formulas.
