Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring
Konstantinos Mamouras, Agnishom Chattopadhyay, Zhifu Wang
Abstract
Abstract We investigate efficient algorithms for the online monitoring of properties written in metric temporal logic (MTL). We employ an abstract algebraic semantics based on semirings. It encompasses the Boolean semantics and a quantitative semantics capturing the robustness of satisfaction, which is based on the max-min semiring over the extended real numbers. We provide a precise equational characterization of the class of semirings for which our semantics can be viewed as an approximation to an alternative semantics that quantifies the distance of a system trace from the set of all traces that satisfy the desired property.
Topics & Concepts
Computer scienceSemantics (computer science)TRACE (psycholinguistics)SemiringTemporal logicRobustness (evolution)Algebraic numberTheoretical computer scienceMetric (unit)Programming languageDiscrete mathematicsMathematicsPhilosophyBiochemistryEconomicsChemistryOperations managementMathematical analysisLinguisticsGeneFormal Methods in VerificationLogic, programming, and type systemsAdvanced Database Systems and Queries