4 papers
Neurosymbolic Feature Extraction for Identifying Forced Labor in Supply Chains
Zili Wang, Frank Montabon, Kristin Yvonne Rozier
Supply chain networks are complex systems that are challenging to analyze; this problem is exacerbated when there are illicit activities involved in the supply chain, such as count…
Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier
Mission-time Linear Temporal Logic (MLTL), a widely used subset of popular specification logics like STL and MTL, is often used to model and verify real world systems in safety-cri…
Formalizing MLTL Formula Progression in Isabelle/HOL
Katherine Kosaian, Zili Wang, Elizabeth Sloan +1
Mission-time Linear Temporal Logic (MLTL) is rapidly increasing in popularity as a specification logic, e.g., for runtime verification and model checking, driving a need for a trus…
Stalnaker's Epistemic Logic in Isabelle/HOL
Laura P. Gamboa Guzman, Kristin Y. Rozier
The foundations of formal models for epistemic and doxastic logics often rely on certain logical aspects of modal logics such as S4 and S4.2 and their semantics; however, the corre…