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 (LTL<sub>f</sub>). Human-readable declarative languages also help the common practitioner to express temporal constraints in a stra...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2024-01-01
|
| Series: | Information |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2078-2489/15/1/34 |
| _version_ | 1797343390615994368 |
|---|---|
| author | Giacomo Bergami |
| author_facet | Giacomo Bergami |
| author_sort | Giacomo Bergami |
| collection | DOAJ |
| description | Recent findings demonstrate how database technology enhances the computation of formal verification tasks expressible in linear time logic for finite traces (LTL<sub>f</sub>). 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 LTL<sub>f</sub> 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 xtLTL<sub>f</sub>-derived algebraic operators. |
| first_indexed | 2024-03-08T10:46:54Z |
| format | Article |
| id | doaj.art-17119026e09e49d0a64fe016579eee94 |
| institution | Directory Open Access Journal |
| issn | 2078-2489 |
| language | English |
| last_indexed | 2024-03-08T10:46:54Z |
| publishDate | 2024-01-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Information |
| spelling | doaj.art-17119026e09e49d0a64fe016579eee942024-01-26T17:03:44ZengMDPI AGInformation2078-24892024-01-011513410.3390/info15010034Streamlining Temporal Formal Verification over Columnar DatabasesGiacomo Bergami0School of Computing, Faculty of Science, Agriculture and Engineering, Newcastle University, Newcastle upon Tyne NE4 5TG, UKRecent findings demonstrate how database technology enhances the computation of formal verification tasks expressible in linear time logic for finite traces (LTL<sub>f</sub>). 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 LTL<sub>f</sub> 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 xtLTL<sub>f</sub>-derived algebraic operators.https://www.mdpi.com/2078-2489/15/1/34temporal formal verificationcolumnar databasesverified artificial intelligencelinear time logic for finite traces |
| spellingShingle | Giacomo Bergami Streamlining Temporal Formal Verification over Columnar Databases Information temporal formal verification columnar databases verified artificial intelligence linear time logic for finite traces |
| title | Streamlining Temporal Formal Verification over Columnar Databases |
| title_full | Streamlining Temporal Formal Verification over Columnar Databases |
| title_fullStr | Streamlining Temporal Formal Verification over Columnar Databases |
| title_full_unstemmed | Streamlining Temporal Formal Verification over Columnar Databases |
| title_short | Streamlining Temporal Formal Verification over Columnar Databases |
| title_sort | streamlining temporal formal verification over columnar databases |
| topic | temporal formal verification columnar databases verified artificial intelligence linear time logic for finite traces |
| url | https://www.mdpi.com/2078-2489/15/1/34 |
| work_keys_str_mv | AT giacomobergami streamliningtemporalformalverificationovercolumnardatabases |