| 1. |
- Dechesne, Francien, et al.
(författare)
-
Interpreted Systems Semantics for Process Algebra with Identity Annotations
- 2013
-
Ingår i: Logic, Language, and Computation. - Heidelberg : Springer Berlin/Heidelberg. - 9783642369759 - 9783642369766 ; , s. 182-205
-
Bokkapitel (refereegranskat)abstract
- Process algebras have been developed as formalisms for specifying the behavioral aspects of protocols. Interpreted systems have been proposed as a semantic model for multi-agent communication. In this paper, we connect these two formalisms by defining an interpreted systems semantics for a generic process algebraic formalism. This allows us to translate and compare the vast body of knowledge and results for each of the two formalisms to the other and perform epistemic reasoning, e.g., using model-checking tools for interpreted systems, on process algebraic specifications. Based on our translation we formulate and prove some results about the interpreted systems generated by process algebraic specifications. © 2013 Springer-Verlag.
|
|
| 2. |
- Dechesne, Francien, et al.
(författare)
-
Operational and epistemic approaches to protocol analysis : bridging the gap
- 2007
-
Ingår i: Logic for Programming, Artificial Intelligence, and Reasoning. - Berlin : Springer Berlin/Heidelberg. - 9783540755586 - 9783540755609 ; , s. 226-241
-
Konferensbidrag (refereegranskat)abstract
- Operational models of protocols, on one hand, are readable and conveniently match their implementation, at a certain abstraction level. Epistemic models, on the other hand, are appropriate for specifying knowledge-related properties such as anonymity. These two approaches to specification and analysis have so far developed in parallel and one has either to define ad hoc correctness criteria for the operational model or use complicated epistemic models to specify the operational behavior. We work towards bridging this gap by proposing a combined framework which allows modeling the behavior of a protocol in a process language with an operational semantics and supports reasoning about properties expressed in a rich logic with temporal and epistemic operators.
|
|
