10.5 Future Work
10.5.2 Extension of the Proof
It would perhaps be desirable to extend the proof of correctness of the core algorithm to cover the full, more complex algorithm for which only informal arguments have been given. Also, a formal proof could be given for the algorithm for finding the bound on the model length for a certain class of formulas, as given in Figure 5.1 on page 55.
1Depending on the chosen type of formula recurrence recognition, see Section 7.5.4 on page 67.
Chapter 11
Conclusion
We have implemented a tool, the BMC/DCValidator, for automated validation of formulas of the DC logic. The BMC/DCValidator translates DC formulas to propositional logic or linear constraint system that may be solved by an external solver.
The work programme that was set out for us demanded an efficient imple-mentation of the ideas of [MF02], including extensions such as the identification of common subexpressions and semantics-preserving simplifications. We have implemented all of these requirements, including some optimisations for spe-cific output formats, and benchmarks have shown that the BMC/DCValidator performs well on various interesting cases.
In addition to the requirements of the work programme, we have constructed a formal proof for the correctness of the core translation algorithm of the BMC/DCValidator. Informal arguments have been provided for the extension to the full, more complex algorithm. The implementation has undergone thor-ough automated and manual tests from several different angles to ensure its proper behaviour.
Conclusively, we are therefore very pleased with the results of this project and of the extent to which we have solved the given assignment.
Bibliography
[AS01] A. C. Shaw:
Real-Time Systems and Software John Wiley & Sons, Inc., 2001.
[ASU86] A. V. Aho, R. Sethi, J. D. Ullman:
Compilers — Principles, Techniques and Tools Addison-Wesley, 1986.
[Ba95] P. Barth:
A Davis-Putnam Enumeration Algorithm for Linear Pseudo-Boolean Op-timization
Technical Report MPI-I-95-2-003, Max-Plack-Institut for Informatik, Saarbr¨ucken, Germany, 1995.
[BDL] G. Behrmann, A. David, K. G. Larsen:
A Tutorial on Uppaal http://www.uppaal.com
[CHR91] Z. Chaochen, C. A. R. Hoare, A. P. Ravn:
A Calculus of Durations
InInformation Processing Letters, 40(5):269-276, 991.
[DLL62] M. Davis, G. Logemann, D. Loveland:
A Machine Program for Theorem Proving InCommunications of the ACM 5(7), 1962.
[DP60] M. Davis, H. Putnam:
A Computing Procedure for Quantification Theory InJournal of the ACM, 7:210-205, 1960.
[DSE] Dedicated Systems Encyclopedia http://www.omnio.be/encyc/
[FH03] M. Fr¨anzle, C. Herde:
Efficient SAT Engines for Concise Logics: Accelerating Proof Search for Zero-One Linear Constraint Systems
In A. Voronkov, ed., Logic for Programming, Artificial Intelligence and Reasoning, volume 2850 ofLNCS, subseries LNAI, pages 302-316. Springer Verlag, sep 2003.
[FH04] M. Fr¨anzle, C. Herde:
Efficient Proof Engines for Bounded Model Checking of Hybrid Systems 2004.
BIBLIOGRAPHY [HA97] H. R. Andersen:
An Introduction to Binary Decision Diagrams 1997/98.
http://www.it.dtu.dk/˜hra/
[JCup] CUP Parser Generator for Java
http://www.cs.princeton.edu/˜appel/modern/java/CUP/
[JK98] J.-P. Katoen: Concepts, Algorithms, and Tools for Model Checking Friedrich-Alexander Universit¨at Erlangen-N¨urnberg, Lecture Notes 1998/99.
[JLex] JLex: A Lexical Analyzer for Java
http://www.cs.princeton.edu/˜appel/modern/java/JLex/
[JUnit] JUnit Regression Testing Framework http://www.junit.org
[JW] M. C. Daconta:
When Runtime.exec() won’t JavaWorld, December 2000.
http://www.javaworld.com/javaworld/jw-12-2000/jw-1229-traps.html [LP00] K. G. Larsen, P. Pettersson:
Timed and Hybrid Systems in UPPAAL2K Presentation given at MOVEP’2k, 2000.
http://www.uppaal.com [MF02] M. Fr¨anzle:
Take it NP-easy: Bounded Model Construction for Duration Calculus InLecture Notes in Computer Science, vol. 2469. Springer-Verlag, 2002.
[MF04] M. Fr¨anzle:
Exam project “Bounded Model Construction for Duration Calculus”
http://www.imm.dtu.dk/cs/eksamensprojekter/E2004/1110.htm [PG86] D. A. Plaisted, S. Greenbaum:
A Structure-Preserving Clause Form Translation InJournal of Symbolic Computation, 2:293-304, 1986.
[SPC04] B. Sharma, P. K. Pandya, S. Chakraborty:
Bounded Validity Checking of Interval Duration Logic 2004.
[TR02] T. M. Rasmussen:
Interval Logic — Proof Theory and Theorem Proving
Ph. D. Thesis, Informatics and Mathematical Modelling, DTU, 2002.
[Tse68] G. Tseitin:
On the Complexity of Derivations in Propositional Calculus
In A. Slisenko, ed.,Studies in Constructive Mathematics and Mathematical Logics, 1968.
[UPP] UPPAAL Homepage http://www.uppaal.com
BIBLIOGRAPHY [WI] Wikipedia, the free encyclopedia
http://en.wikipedia.org/wiki/
[ZH04] Z. Chaochen, M. R. Hansen:
Duration Calculus — A Formal Approach to Real-Time Systems Springer-Verlag, 2004.
Appendix A
Symbol Index
The symbol index references the page where a given symbol was defined.
Symbol Signature Description Page
DC The set of duration calculus
for-mulas
7
SA The set of state assertions 7
State The set of states 7
Time N Time 7
LitSA The set of literals
represent-ing state assertions at particular time instants
16
LitDC The set of literals
represent-ing duration calculus formulas at particular time intervals
16
Lit The union ofLitSAandLitDC 16
LitSA The extension of LitSA to
boolean combinations of the lit-erals
17
LitDC The extension of LitDC to
boolean combinations of the lit-erals
17
Lit The extension ofLit to boolean
combinations of the literals
17
φ,φi,ψ DC Duration calculus formula 7
S,Si SA State assertion 7
σ State→B Valuation of states 8
ˆ
σ LitSA→B Valuation of literals representing
state assertions
19 ˆ
σ LitSA→B Valuation of boolean
combina-tions of literals representing state assertions
20
APPENDIX A. SYMBOL INDEX
ρ Time →State→B Trajectory, i.e. time-dependent valuation of states
7
˜
ρ Lit→B Valuation of literals 25
˜
ρ Lit→B Valuation of boolean
combina-tions of literals
25
ξ Lit→B Valuation of literals 25
←
ξ Time →State→B Trajectory, i.e. time-dependent valuation of states
23
I[[S]](σ) B Interpretation ofS in σ 8
ρ,[i, j]|=φ B Observation (ρ,[i, j]) satisfiesφ 7
[S]i LitSA Literal 16
[φ]i,j LitDC Literal 16
[φ_ψ]i,m,j LitDC Literal 41
[true] Lit Literal 18
xi,yi Lit Literal 13
ai N\ {0} Weight 13
V P(State) Set of state variables 10
_ DC×DC→DC Chop 7
RS≥n DC Duration formula 7
tkDC[[φ]] Lit Translation of subformulaφ 17
tkDC,p[[φ]] Lit Translation of subformulaφwith polarityp
36
tkSA[[S]] LitSA Translation of S 18
tkSA,p[[S]] LitSA Translation of Swith polarity p 36
BM C[[φ, k]] Lit Complete translation ofφ 18
2 DC →DC For all subintervals 9
3 DC →DC For some subinterval 9
φ→ψ Simplification rule 48
Appendix B
Complexity Classes
In this appendix, we shall briefly describe the different complexity classes that are referenced in this thesis. The contents of this chapter are based on [WI].
B.1 The P and NP Complexity Classes
A decision problem that can be solved in polynomial time by a determinis-tic machine is said to be a member of the polynomial (P) complexity class.
Equivalently, a decision problem that can be solved in polynomial time by a non-deterministic machine is said to be a member of the non-deterministic polynomial (NP) complexity class.
The relation between the two classes is P ⊆NP. It is commonly believed that P is in fact a proper subset of NP, but this claim has not been proven.
Decision problems in the complexity class NP-hard are those problems which are at least as hard as any problem in NP.
The NP-complete problems are the hardest problems in NP, i.e. the inter-section between the complexity classes NP and NP-hard.