Equational Reasoning on Mobile Ad Hoc Networks

• Autorzy: Ghassemi F. , Fokkink W. , Movaghar A.
• Języki publikacji: EN

Abstrakty

EN

We provide an equational theory for Restricted Broadcast Process Theory to reason about ad hoc networks. We exploit an extended algebra called Computed Network Theory to axiomatize restricted broadcast. It allows one to define the behavior of an ad hoc network with respect to the underlying topologies. We give a sound and ground-complete axiomatization for CNT terms with finite-state behavior, modulo what we call rooted branching computed network bisimilarity.

Słowa kluczowe

EN

Computed Network Theory; operational semantics; Restricted Broadcast Process Theory; Computed Network Bisimulation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 105, nr 4
• Strony: 375--415
• Opis fizyczny: Bibliogr. 26 poz., tab., wykr.

Twórcy

autor

Ghassemi F.

autor

Fokkink W.

autor

Movaghar A.

• Sharif University of Technology Tehran, Iran,

Bibliografia

• [1] Baeten, J., Bravetti, M.: A Ground-Complete Axiomatization of Finite State Processes in Process Algebra, Proc. 16th Conference on Concurrency Theory (CONCUR), LNCS 3653, pages 248-262, Springer, 2005.
• [2] Basten, T.: Branching Bisimilarity is an Equivalence Indeed!, Information Processing Letters, 58(3), 1996, 141-147.
• [3] Bergstra, J., Klop, J.: Process Algebra for Synchronous Communication, Information and Control, 60(1-3), 1984, 109-137.
• [4] Ehrich, H., Loeckx, J., Wolf, M.: Specification of Abstract Data Types, John Wiley, 1996.
• [5] Ene, C., Muntean, T.: A Broadcast-based Calculus for Communicating Systems, Proc. 15th Parallel & Distributed Processing Symposium (IPDPS), page 149, IEEE, 2001.
• [6] Ghassemi, F., Fokkink, W., Movaghar, A.: Restricted Broadcast Process Theory, Proc. 6th Conference on Software Engineering and Formal Methods (SEFM), pages 345-354, IEEE, 2008.
• [7] Ghassemi, F., Fokkink,W.,Movaghar,A.: Equational Reasoning on Ad Hoc Networks, Proc. 3rd Conference on Fundamentals of Software Engineering (FSEN), LNCS 5961, pages 113-128, Springer, 2009.
• [8] van Glabbeek, R.: A Complete Axiomatization for Branching Bisimulation Congruence of Finite-State Behaviours, Proc. 18th Symposium on Mathematical Foundations of Computer Science (MFCS), LNCS 711, pages 473-484, Springer, 1993.
• [9] van Glabbeek, R.: Notes on theMethodology of CCS and CSP, Theoretical Computer Science, 177(2), 1997, 329-349.
• [10] van Glabbeek, R., Weijland, W.: Branching Time and Abstraction in Bisimulation Semantics, Journal of the ACM, 43(3), 1996, 555-600.
• [11] Godskesen, J.: A Calculus forMobile Ad Hoc Networks, Proc. 9th Conference on Coordination Models and Languages (COORDINATION), LNCS 4467, pages 132-150, Springer, 2007.
• [12] Godskesen, J.: A Calculus for Mobile Ad-hoc Networks with Static Location Binding, Electronic Notes in Theoretical Computer Science, 242(1), 2009, 161-183.
• [13] Godskesen, J., Nanz, S.: Mobility Models and Behavioural Equivalence for Wireless Networks, Proc. 11th Conference on Coordination Models and Languages (COORDINATION), LNCS 5521, pages 106-122, Springer, 2009.
• [14] Godskesen, J. C.: Observables for Mobile and Wireless Broadcasting Systems, Proc. 12th Conference on Coordination Models and Languages (COORDINATION), LNCS 6116, pages 1-15, Springer, 2010.
• [15] Groote, J., Mathijssen, A., Reniers, M. A., Usenko, Y. S., van Weerdenburg, M.: The Formal Specification Language mCRL2, Proc. Methods for Modelling Software Systems (MMOSS), vol. 06351 of Dagstuhl Seminar Proceedings, 2006.
• [16] Groote, J., Ponse, A.: μCRL: A Base for Analysing Processes with Data, Proc. 3rdWorkshop on Concurrency and Compositionality, pages 125-130, GMD-Studien Nr. 191, 1991.
• [17] Groote, J., Ponse, A.: Proof Theory for μCRL: A Language for Processes with Data, Semantics of Specification Languages,Workshops in Computing, pages 232-251, Springer, 1993.
• [18] Groote, J., Ponse, A.: Syntax and Semantics of μ-CRL, Algebra of Communicating Processes, Workshops in Computing, pages 26-62, Springer, 1995.
• [19] Hojjat, H., Mousavi, M. R., Sirjani, M.: A Framework for Performance Evaluation and Functional Verification in Stochastic Process Algebras, Proc. ACM Symposium on Applied Computing (ACM SAC), pages 339-346, ACM, 2008.
• [20] Merro, M.: An Observational Theory for Mobile Ad Hoc Networks, Information and Computation, 207(2), 2009, 194-208.
• [21] Merro, M., Sibilio, E.: A Timed Calculus for Wireless Systems, Proc. 3rd Conference on Fundamentals of Software Engineering (FSEN), LNCS 5961, pages 228-243, Springer, 2010.
• [22] Mezzetti, N., Sangiorgi, D.: Towards a Calculus For Wireless Systems, Electronic Notes in Theoretical Computer Science, 158, 2006, 331-353.
• [23] Milner, R.: A Complete Axiomatisation for ObservationalCongruence of Finite-State Behaviors, Information and Computation, 81(2), 1989, 227-247.
• [24] Nanz, S., Hankin, C.: A Framework for Security Analysis of Mobile Wireless Networks, Theoretical Computer Science, 367(1), 2006, 203-227.
• [25] Park, D.: Concurrency and Automata on Infinite Sequences, Proc. 5th GI-Conference on Theoretical Computer Science, LNCS 104, pages 167-183, Springer, 1981.
• [26] Singh, A., Ramakrishnan, C. R., Smolka, S. A.: A Process Calculus for Mobile Ad Hoc Networks, Science of Computer Programming, 75(6), 2010, 440-469.