Doctoral Dissertation Temporal Linear Logic and Its Applications

Linear logic, introduced by Girard in 1987, has been called a resource conscious logic. In order to express a dynamic change in process environment, it is useful to consider a concept of resource such as data consumption. The expressive power of linear logic is evidenced by some very natural encodings of computational models such as Petri nets, counter machines, Turing machines, and others. For example, in Petri nets, tokens are considered as resources that are consumed and transitions are considered as reusable resources. It is well known that the reachability problem for ordinary Petri nets is equivalent to the provability for the corresponding sequent of linear logic. Also, as a formal logical system, linear logic satisfies some basic theorems. In it the cut elimination theorem and the soundness and completeness theorems for phase semantics which is a standard semantics of linear logic hold true. In particular, the cut elimination theorem can be applied to logic programming, uniform proof and proof search, and so on. We think that linear logic has been given various applications in computer science through its resource consciousness and usefulness as a formal system. However, since linear logic does not include a concept of time directly, it is not enough to treat a dynamic change in environments with the passage of time such as execution time and waiting time