Expressing and Verifying Temporal and Structural Properties of Mobile Agents

• Autorzy: Bednarczyk M.A. , Jamroga W. , Pawłowski W.
• Języki publikacji: EN

Abstrakty

EN

Logics for expressing properties of Petri hypernets, a visual formalism for modelling mobile agents, are proposed. Two classes of properties are of interest-the temporal evolution of agents and their structural correlation. In particular, we investigate how the classes can be combined into a logic capable of expressing the dynamic evolution of the structural correlation. The problem of model checking properties of a class of the logic on Petri hypernets is shown to be pspace-complete.

Słowa kluczowe

EN

dynamic mobile agents; Petri hypernets; temporal logic; model checking

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 72, nr 1-3
• Strony: 51--63
• Opis fizyczny: wykr., bibliogr. 24 poz.

Twórcy

autor

Bednarczyk M.A.

autor

Jamroga W.

autor

Pawłowski W.

• Institut of Computer Science, Polish Academy of Science, A.Abrahama 18, 81-825 Sopot, Poland,

Bibliografia

• [1] Bednarczyk, M., Bernardinello, L., Pawłowski, W., Pomello, L.: Modelling Mobility with Petri Hypernets, Proceedings of WADT 2004, 3423, 2004.
• [2] Bednarczyk, M. A., Bernardinello, L., Pawłowski, W., Pomello, L.: Petri hypernets explained, 2006, Submitted to ATPN'06.
• [3] Bednarczyk,M. A., Jamroga,W., Pawłowski,W.: Expressing and Verifying Temporal and Structural Properties ofMobile Agents, Proceedings of the Concurrency, Specification and ProgrammingWorkshop CS&P'05 (L. Czaja, Ed.), 2005.
• [4] Bednarczyk, M. A., Jamroga, W., Pawłowski, W.: Expressing and Verifying Temporal and Structural Properties of Mobile Agents, Technical Report IfI-05-09, Clausthal University of Technology, 2005.
• [5] Cardelli, L., Gordon, A. D.: Mobile Ambients., Electr. Notes Theor. Comput. Sci., 10, 1997.
• [6] Charatonik, W., Dal-Zilio, S., Gordon, A. D., Mukhopadhyay, S., Talbot, J.-M.: Model checking mobile ambients., Theor. Comput. Sci., 308(1-3), 2003, 277-331.
• [7] Clarke, E., Emerson, E.: Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic, Proceedings of Logics of Programs Workshop, 131, 1981.
• [8] Emerson, E., Halpern, J.: "Sometimes" and "Not Never" Revisited: On Branching versus Linear Time Temporal Logic, Journal of the ACM, 33(1), 1986, 151-178.
• [9] Emerson, E. A.: Temporal and Modal Logic, in: Handbook of Theoretical Computer Science (J. van Leeuwen, Ed.), vol. B, Elsevier Science Publishers, 1990, 995-1072.
• [10] Esparza, J.: Decidability of Model Checking for Infinite-State Concurrent Systems., Acta Inf., 34(2), 1997, 85-107.
• [11] Esparza, J.: Decidability and Complexity of Petri Net Problems. An introduction, in: Lectures on Petri Nets I: Basic Models. Adv. in Petri Nets (G. Rozenberg, W. Reisig, Eds.), vol. 1491 of LNCS, Springer Verlag, 1998, 374-428.
• [12] Franceschet, M., Montanari, A., de Rijke, M.: Model Checking for Combined Logics with an Application to Mobile Systems., Autom. Softw. Eng., 11(3), 2004, 289-321.
• [13] Gabbay, D. M.: Fibring Logics, vol. 38 of Oxford Logic Guides, Oxford Univesity Press, 1998.
• [14] Gabbay, D. M., Pnuelli, A., Shelah, S., Stavi, J.: On the Temporal Analysis of Fairness, Proceedings of POPL'80, 1980.
• [15] Gabbay, D. M., Shehtman, V.: Products of modal logics, Part 1, Logic Journal of the IGPL, 6(1), 1998, 73-146.
• [16] Kracht, M., Wolter, F.: Properties Of Independently Axiomatizable Bimodal Logics, Journal Of Symbolic Logic, 54 (4), 1991, 1469-1485.
• [17] Kupferman, O., Vardi, M., Wolper, P.: An automata-theoretic approach to branching-time model checking, Journal of the ACM, 47(2), 2000, 312-360.
• [18] McMillan, K.: Symbolic Model Checking: An Approach to the State Explosion Problem, Kluwer Academic Publishers, 1993.
• [19] McMillan, K.: Applying SAT Methods in Unbounded Symbolic Model Checking, Proceedings of CAV'02, 2404, 2002.
• [20] Rao, A., Georgeff, M.: Modeling Rational Agents within a BDI-Architecture, Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning, 1991.
• [21] Reisig, W.: Petri Nets, vol. 4 of EATCS Monographs on Theoretical Computer Science, Springer-Verlag, 1985.
• [22] Schild, K.: On the Relationship Between BDI Logics and Standard Logics of Concurrency, Autonomous Agents and Multi Agent Systems, 2000, 259-283.
• [23] Schnoebelen, P.: The Complexity of Temporal Model Checking, Advances in Modal Logics, Proceedings of AiML 2002,World Scientific, 2003.
• [24] Valk, R.: Petri Nets as Token Objects: An Introduction to Elementary Object Nets, Applications and Theory of Petri Nets 1998, Proceedings (W. van der Aalst, E. Best, Eds.), 1420, Springer-Verlag, 1998.