Symbolic model checking of public announcement protocols

We study the symbolic model checking problem against public announcement protocol logic (PAPL), featuring protocols with public announcements, arbitrary public announcements and group announcements. Technically, symbolic models are Kripke models whose accessibility relations are presented as programs described in a dynamic logic style with propositional assignments. We highlight the relevance of such symbolic models and show that the symbolic model checking problem against PAPL is A$_{\textrm{pol}}$Exptime-complete as soon as announcement protocols allow for either arbitrary announcements or iteration of public announcements. However, when both options are discarded, the complexity drops to Pspace-complete.

Novel Protocol Model Design of Wireless Sensor Real-Time Control Network

Wireless sensor real-time control network is important construction part. With same Real-time system, this network need Real-time and reliability. Modern network mainly is Ethernet. This network speed is fast than the older, the simple protocol, the lower cost and integrate TCP/IP technique in the IT world. But because its self mechanism decide that it is a no-realtime network. This paper propose a novel wireless sensor real-time control network protocol model based on Ethernet hardware, including protocol logic, communication strategy logic, server logic, communication control logic and CMIB. At the same time, this paper introduce work flows and main function of main constructing part of this real-time protocol model.