PROVING FINITENESS OF CCS PROCESSES BY NONSTANDARD SEMANTICS

被引：3

作者：

DEFRANCESCO, N ^{[1
]}

INVERARDI, P ^{[1
]}

机构：

[1] CNR,IEI,I-56100 PISA,ITALY

来源：

ACTA INFORMATICA | 1994年 / 31卷 / 01期

关键词：

D O I：

10.1007/BF01178922

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We present a semantic method to check the finiteness of CCS terms. The method is interpretative, i.e. it is based on a non-standard CCS operational semantics. According to this semantics it is always possible, given a process p, to build a finite state transition system which, if a condition holds, is a finite representation of p, otherwise it is a suitable approximation of its semantic behaviour. The method is able to decide the finiteness of a CCS term in a larger number of cases than those captured by known syntactic criteria.

引用

页码：55 / 80

页数：26

共 15 条

[1]

ABRAMSKY S, 1987, ABSTRACT INTERPRETAT

[2] PROCESS ALGEBRA FOR SYNCHRONOUS COMMUNICATION [J].

BERGSTRA, JA ;

KLOP, JW .

INFORMATION AND CONTROL, 1984, 60 (1-3) :109-137

[3]

Bolognesi T., 1989, Formal Description Techniques. Proceedings of the First International Conference, P201

[4] INTRODUCTION TO THE ISO SPECIFICATION LANGUAGE LOTOS [J].

BOLOGNESI, T ;

BRINKSMA, E .

COMPUTER NETWORKS AND ISDN SYSTEMS, 1987, 14 (01) :25-59

[5]

BOLOGNESI T, 1987, 7TH P IFIP WG 6 1 C

[6]

CLEAVELAND R, 1988, CONCURRENCY WORKBENC

[7]

DEFRANCESCO N, 1991, LECT NOTES COMPUT SC, V575, P266

[8]

DESIMONE R, 1989, INRIA11 TECHN REP

[9]

FERNANDEZ J, 1988, THESIS U GRENOBLE

[10]

GROOTE JF, 1990, LECT NOTES COMPUT SC, V443, P626

← 1 2 →