Issue with checking not(phi)

roberthsheng / STL-SMTLIB

STL to SMT-LIB compiler based on definitions from "A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation"

https://publications.cispa.saarland/3654/1/algorithms-15-00126-v2.pdf

0 stars 0 forks source link

Issue with checking not(phi) #17

Closed roberthsheng closed 1 year ago

roberthsheng commented 1 year ago

We finally add one of the two conjuncts (a) ¬φ_t′ or (b) φ_t′ alternatively, where t′ = t − duration(φ), to the resultant constraint system and check both variants for their satisfiability using an SMT-LA solver. Depending on the results of the two satisfiability checks, we report

inconclusive if both systems are found to be satisfiable,
⊤ if the system (a) containing ¬φ_t′ is unsatisfiable,
⊥ if the system (b) containing φ_t′ is unsatisfiable.

roberthsheng commented 1 year ago

When not(phi) is checked for sat, you can just set an introduced boolean subvariable p_n as the opposite boolean value to satisfy the formula