Extracting proofs from tabled proof search
We consider the problem of model checking specifications involving co-inductive definitions such as are available for bisimulation. A proof search approach to model checking with such specifications often involves state exploration. We consider four different tabling strategies that can minimize su...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Conference Paper |
| Language: | English |
| Published: |
2013
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/10356/98261 http://hdl.handle.net/10220/18356 |
| _version_ | 1811681983135219712 |
|---|---|
| author | Miller, Dale. Tiu, Alwen. |
| author2 | School of Computer Engineering |
| author_facet | School of Computer Engineering Miller, Dale. Tiu, Alwen. |
| author_sort | Miller, Dale. |
| collection | NTU |
| description | We consider the problem of model checking specifications involving co-inductive definitions such as are available for bisimulation. A proof search approach to model checking with such specifications often involves state exploration. We consider four different tabling strategies that can minimize such exploration significantly. In general, tabling involves storing previously proved subgoals and reusing (instead of reproving) them in proof search. In the case of co-inductive proof search, tables allow a limited form of loop checking, which is often necessary for, say, checking bisimulation of non-terminating processes. We enhance the notion of tabled proof search by allowing a limited deduction from tabled entries when performing table lookup. The main problem with this enhanced tabling
method is that it is generally unsound when co-inductive definitions are involved and when tabled entries contain unproved entries. We design a proof system with tables and show that by managing tabled entries carefully, one would still be able to obtain a sound proof system. That is, we show how one can extract a post-fixed point from a tabled proof for a co-inductive goal. We then apply this idea to the technique of bisimulation ``up-to'' commonly used in process algebra. |
| first_indexed | 2024-10-01T03:49:36Z |
| format | Conference Paper |
| id | ntu-10356/98261 |
| institution | Nanyang Technological University |
| language | English |
| last_indexed | 2024-10-01T03:49:36Z |
| publishDate | 2013 |
| record_format | dspace |
| spelling | ntu-10356/982612020-05-28T07:17:41Z Extracting proofs from tabled proof search Miller, Dale. Tiu, Alwen. School of Computer Engineering International Conference of Certified Programs and Proofs (3rd : 2013 : Melbourne, Australia) DRNTU::Engineering::Computer science and engineering We consider the problem of model checking specifications involving co-inductive definitions such as are available for bisimulation. A proof search approach to model checking with such specifications often involves state exploration. We consider four different tabling strategies that can minimize such exploration significantly. In general, tabling involves storing previously proved subgoals and reusing (instead of reproving) them in proof search. In the case of co-inductive proof search, tables allow a limited form of loop checking, which is often necessary for, say, checking bisimulation of non-terminating processes. We enhance the notion of tabled proof search by allowing a limited deduction from tabled entries when performing table lookup. The main problem with this enhanced tabling method is that it is generally unsound when co-inductive definitions are involved and when tabled entries contain unproved entries. We design a proof system with tables and show that by managing tabled entries carefully, one would still be able to obtain a sound proof system. That is, we show how one can extract a post-fixed point from a tabled proof for a co-inductive goal. We then apply this idea to the technique of bisimulation ``up-to'' commonly used in process algebra. 2013-12-23T03:37:39Z 2019-12-06T19:52:54Z 2013-12-23T03:37:39Z 2019-12-06T19:52:54Z 2013 2013 Conference Paper Miller, D., & Tiu, A. (2013). Extracting Proofs from Tabled Proof Search. Third International Conference, CPP 2013, Melbourne, VIC, Australia, 8307, pp.194-210. https://hdl.handle.net/10356/98261 http://hdl.handle.net/10220/18356 10.1007/978-3-319-03545-1_13 en © 2013 Springer International Publishing Switzerland |
| spellingShingle | DRNTU::Engineering::Computer science and engineering Miller, Dale. Tiu, Alwen. Extracting proofs from tabled proof search |
| title | Extracting proofs from tabled proof search |
| title_full | Extracting proofs from tabled proof search |
| title_fullStr | Extracting proofs from tabled proof search |
| title_full_unstemmed | Extracting proofs from tabled proof search |
| title_short | Extracting proofs from tabled proof search |
| title_sort | extracting proofs from tabled proof search |
| topic | DRNTU::Engineering::Computer science and engineering |
| url | https://hdl.handle.net/10356/98261 http://hdl.handle.net/10220/18356 |
| work_keys_str_mv | AT millerdale extractingproofsfromtabledproofsearch AT tiualwen extractingproofsfromtabledproofsearch |