International collaborative studies on a logical specification and verification language.

我们开发和设计了一个正式的规范和验证工具的动态实时系统的合作与法国的合作伙伴组（Jean-Pierre Jouannaud的组），基于线性逻辑。动态实时系统是指参与的Agent数量和时间约束可以动态变化的多Agent系统。我们给出了一个自动化的转换过程，将用户级的自然规范转换为线性逻辑规范。我们还给出了一个消除过程，以消除从线性逻辑规范的密集时间概念。然后，根据线性逻辑片段的证明搜索机制执行各种验证。密集时间消除过程是由构造性逻辑中已知的程序提取方法给出的。我们还开发了一个逻辑框架的安全协议的正确性证明，应用相同的概念。我们还研究了一些相关的逻辑研究，我们的线性逻辑，这是我们的验证工具的逻辑框架。

We developed and designed a formal specification and verification tool for dynamic real-time systems in the collaboration with the French partner group (Jean-Pierre Jouannaud's group), based on linear logic. By dynamic real-time systems we mean a multi-agent systems in which the number of participating agents may be changed and the time constraints may be changed dynamically We gave an automated transformation procedure to transform a natural specification on the user-level into a linear logical specification. We also gave an elimination procedure to eliminate the dense time notions from a linear logical specification. Then, various kinds of verifications are performed in terms of the proof-search mechanism of a fragment of linear logic. The dense time elimination procedure is given by a program extraction method known in constructive logic. We also developed a logical framework for the security protocol correctness proofs, applying the same concept. We also studied some related logical research on our linear logic, which is the logical framework of our verification tool.