Linear-time Temporal Logic with Event Freezing Functions
Formal properties represent a cornerstone of the system-correctness proofs based on formal verification techniques such as model checking. Formalizing requirements into temporal properties may be very complex and error prone, due not only to the ambiguity of the textual requirements but also to the...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2017-09-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1709.02103v1 |
| _version_ | 1818262781656301568 |
|---|---|
| author | Stefano Tonetta |
| author_facet | Stefano Tonetta |
| author_sort | Stefano Tonetta |
| collection | DOAJ |
| description | Formal properties represent a cornerstone of the system-correctness proofs based on formal verification techniques such as model checking. Formalizing requirements into temporal properties may be very complex and error prone, due not only to the ambiguity of the textual requirements but also to the complexity of the formal language. Finding a property specification language that balances simplicity, expressiveness, and tool support remains an open problem in many real-world contexts.
In this paper, we propose a new temporal logic, which extends First-Order Linear-time Temporal Logic with Past adding two operators "at next" and "at last", which take in input a term and a formula and represent the value of the term at the next state in the future or last state in the past in which the formula holds. We consider different models of time (including discrete, dense, and super-dense time) and Satisfiability Modulo Theories (SMT) of the first-order formulas. The "at next" and "at last" functions can be seen as a generalization of Event-Clock operators and can encode some Metric Temporal operators also with counting. They are useful to formalize properties of component-based models because they allow to express constraints on the data exchanged with messages at different instants of time. We provide a simple encoding into equisatisfiable formulas without the extra functional symbols. We implement a prototype tool support based on SMT-based model checking. |
| first_indexed | 2024-12-12T19:08:35Z |
| format | Article |
| id | doaj.art-eacc128cdf9a4332946f504dc0987459 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-12T19:08:35Z |
| publishDate | 2017-09-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-eacc128cdf9a4332946f504dc09874592022-12-22T00:14:55ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802017-09-01256Proc. GandALF 201719520910.4204/EPTCS.256.14:22Linear-time Temporal Logic with Event Freezing FunctionsStefano Tonetta0 FBK-irst Formal properties represent a cornerstone of the system-correctness proofs based on formal verification techniques such as model checking. Formalizing requirements into temporal properties may be very complex and error prone, due not only to the ambiguity of the textual requirements but also to the complexity of the formal language. Finding a property specification language that balances simplicity, expressiveness, and tool support remains an open problem in many real-world contexts. In this paper, we propose a new temporal logic, which extends First-Order Linear-time Temporal Logic with Past adding two operators "at next" and "at last", which take in input a term and a formula and represent the value of the term at the next state in the future or last state in the past in which the formula holds. We consider different models of time (including discrete, dense, and super-dense time) and Satisfiability Modulo Theories (SMT) of the first-order formulas. The "at next" and "at last" functions can be seen as a generalization of Event-Clock operators and can encode some Metric Temporal operators also with counting. They are useful to formalize properties of component-based models because they allow to express constraints on the data exchanged with messages at different instants of time. We provide a simple encoding into equisatisfiable formulas without the extra functional symbols. We implement a prototype tool support based on SMT-based model checking.http://arxiv.org/pdf/1709.02103v1 |
| spellingShingle | Stefano Tonetta Linear-time Temporal Logic with Event Freezing Functions Electronic Proceedings in Theoretical Computer Science |
| title | Linear-time Temporal Logic with Event Freezing Functions |
| title_full | Linear-time Temporal Logic with Event Freezing Functions |
| title_fullStr | Linear-time Temporal Logic with Event Freezing Functions |
| title_full_unstemmed | Linear-time Temporal Logic with Event Freezing Functions |
| title_short | Linear-time Temporal Logic with Event Freezing Functions |
| title_sort | linear time temporal logic with event freezing functions |
| url | http://arxiv.org/pdf/1709.02103v1 |
| work_keys_str_mv | AT stefanotonetta lineartimetemporallogicwitheventfreezingfunctions |