Temporal Logic에 대한 그래프 모형 : Concurrent 프로그램의 자동생성 및 검증을 위한 도구 = Graph Model for Temporal Logic : A Tool for Automatic Synthesis and Verification of Concurrent Programs

국문 초록 (Abstract)

본 논문에서는 [3]에서 제안된 그래프 모형을 마크함으로써 eventuality성질을 보다 분명히 표현할 수 있도록 그래프 모형을 구성하는 방법과, 구성된 그래프 모형의 간소화 알고리즘을 제안하였다.
또한 두 개의 프로세스와 synchronizer로 구성된 문제에서 Propositional Temporal Logic으로 표현된 프로그램 사양의 그래프 모형을 구성하고, 그래프 모형이 프로그램의 합성 및 사양의 검증에 이용될 수 있음을 보였다.

다국어 초록 (Multilingual Abstract)

In this paper, for representing eventuality property of PTL (propositional temporal logic), We extend the graph model [3], and we give the minimization algorithm for the extended graph model.
The extension is made by giving node marking and marked node visiting rule to the graph model.
As an example, we construct the extended graph model from the PTL specifications which specify the system of two processes and a synchronizer satisfying mutual exclusion.

목차 (Table of Contents)

• 요약
• ABSTRACT
• 1. 서론
• 2. Temporal Logic
• 3. 그래프 모형의 정의 및 그의 구성
• 4. 그래프 모형의 간소화
• 5. 적용 예
• 6. 결론
• 참고문헌
• 저자소개