Matching Specifications For Message Sequence Charts
FoSSaCS '99: Proceedings of the Second International Conference on Foundations of Software Science and Computation Structure, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99（1999）
摘要
Message sequence charts (MSC) are widely used in the early design of communication protocols. They allow describing the communication skeleton of a system. We consider a basic verification task for hierarchical MSCs, the matching problem via MSC templates. We characterize the complexity of checking properties which are expressible by and-or templates, resp. by LTL formulas. Both problems are shown to be PSPACE-complete.
更多查看译文
关键词
MSC template,communication protocol,communication skeleton,LTL formula,and-or template,basic verification task,early design,hierarchical MSCs,matching problem,message sequence chart,Matching Specifications,Message Sequence Charts
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要