Controller Design from Temporal Logic: Undecidability need not matter |
| | Abstract | Due to rapidly dropping costs and rapidly increasing power and flexibility of embedded digital hardware, digital control becomes more and more extensive in systems encountered in everyday life. However, the interaction between digital controllers and their continuously evolving controlled environment is far from trivial. Therefore, an exact analysis of this interaction is hardly ever pursued; instead, simplified models are used in order to ease analysis. Typical simplifications include that transitions of the embedded controller are assumed to be without duration. This idealization gives rise to a peculiar property of such models, namely that transitions can follow each other arbitrarily close in time, which they cannot in reality. However, intelligent exploitation of exactly this property is the core of many undecidability results in the field. Consequently, some of the intricacy of designing and verifying embedded controllers, as witnessed by these undecidability results, may be an artefact of such an overly idealized formalization rather than inherent to the design task. However, without further justification, this is just a hypothesis.
Based on this scientific hypothesis, the Ph.D. thesis ``Controller Design from Temporal Logic: Undecidability Need Not Matter'' sets out to prove that this hypothesis is actually true and applies to some well-studied design formalisms. The demonstrator formalism used throughout is the core of the Duration Calculi, which is a major group of calculi proposed for the rigorous development of embedded real-time control systems. The Duration Calculi are highly undecidable, but most of these undecidability results rely on the number of discrete state changes in a finite time interval not being finitely bounded. In the thesis, positive decidability results are established for slightly more restrictive model classes, where the additional constraints on the temporal distribution of possible state changes are derived from considerations concerning the physical properties of embedded controllers. In the remainder, these considerations are shown to apply for interesting classes of embedded control circuitry, yielding a procedure for automatically synthesizing synchronous control hardware from specifications in Duration Calculus and a model-checking algorithm for automatically verifying asynchronous circuits against a substantial subset of Duration Calculus.
However, we claim that the impact of these findings goes much deeper than just Duration Calculus. Formal methods are intended to be mathematically rigorous design instruments, aiming at subjecting the development process to mathematical verification. Hence, the only rationale for taking idealizations in the formal representation of a design problem is that the gains in tractability of the problem may outweigh the loss of accuracy. However, if such semantic idealizations complicate rather than simplify the design problem then there is no justification for taking them. Thus, our results may be interpreted as an indication that liberating formal models of embedded control from some of the idealizations that have been imposed for smoothening the models may enhance both their accuracy and their tractability. As this implies that similar analyses of other formal models of embedded-system specification and implementation may yield similar gains, there is quite some potential for extending our results to other temporal logics or even for exploiting them in high-level hardware synthesis technologies. | | Type | Ph.D. thesis [Academic thesis] | | Year | 1997 No. 9710 | | Publisher | | | Address | Kiel, Germany | | Series | | | Electronic version(s) | [ps] | | Publication link | http://www.imm.dtu.dk/~mf/diss.ps.gz | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|