Streamlining Temporal Formal Verification over Columnar Databases
Recent findings demonstrate how database technology enhances the computation of formal verification tasks expressible in linear time logic for finite traces (LTLf). Human-readable declarative languages also help the common practitioner to express temporal constraints in a straightforward and accessible language. Notwithstanding the former, this technology is in its infancy, and therefore, few optimization algorithms are known for dealing with massive amounts of information audited from real systems. We, therefore, present four novel algorithms subsuming entire LTLf expressions while outperforming previous state-of-the-art implementations on top of KnoBAB, thus postulating the need for the corresponding, leading to the formulation of novel xtLTLf-derived algebraic operators.
Code (1)
Similar Papers 제목 키워드 기반
Columnar Database Techniques for Creating AI Features
Recent advances with in-memory columnar database techniques have increased the performance of analytical queries on very large databases and data warehouses. At the same time, advances in artificial intelligence (AI) alg…
feature selectionWhat is Formal Verification without Specifications? A Survey on mining LTL Specifications
Virtually all verification techniques using formal methods rely on the availability of a formal specification, which describes the design requirements precisely. However, formulating specifications remains a manual task …
Enumerative SearchSurveyFormal Verification of Linear Temporal Logic Specifications Using Hybrid Zonotope-Based Reachability Analysis
In this paper, we introduce a hybrid zonotope-based approach for formally verifying the behavior of autonomous systems operating under Linear Temporal Logic (LTL) specifications. In particular, we formally verify the LTL…
JSTR: Joint Spatio-Temporal Reasoning for Event-based Moving Object Detection
Event-based moving object detection is a challenging task, where static background and moving object are mixed together. Typically, existing methods mainly align the background events to the same spatial coordinate syste…
Motion CompensationMoving Object DetectionObjectobject-detection+2Formal Verification of Unknown Stochastic Systems via Non-parametric Estimation
A novel data-driven method for formal verification is proposed to study complex systems operating in safety-critical domains. The proposed approach is able to formally verify discrete-time stochastic dynamical systems ag…