Counterpart Semantics for a Second-Order μ-Calculus

• Autorzy: Gadducci F. , Lafuente A. L. , Vandin A.
• Języki publikacji: EN

Abstrakty

EN

Quantified &mi;-calculi combine the fix-point and modal operators of temporal logics with (existential and universal) quantifiers, and they allow for reasoning about the possible behaviour of individual components within a software system. In this paper we introduce a novel approach to the semantics of such calculi: we consider a sort of labeled transition systems called counterpart models as semantic domain, where states are algebras and transitions are defined by counterpart relations (a family of partial homomorphisms) between states. Then, formulae are interpreted over sets of state assignments (families of partial substitutions, associating formula variables to state components). Our proposal allows us to model and reason about the creation and deletion of components, as well as the merging of components. Moreover, it avoids the limitations of existing approaches, usually enforcing restrictions of the transition relation: the resulting semantics is a streamlined and intuitively appealing one, yet it is general enough to cover most of the alternative proposals we are aware of. The paper is rounded up with some considerations about expressiveness and decidability aspects.

Słowa kluczowe

EN

quantified u-calculi; counterpart semantics; modal logics; graph transformation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2012
• Tom: Vol. 118, nr 1-2
• Strony: 177--205
• Opis fizyczny: Bibliogr. 45 poz., rys.

Twórcy

autor

Gadducci F.

autor

Lafuente A. L.

autor

Vandin A.

• IMT Institute for Advanced Studies Lucca Piazza San Ponziano 6, Lucca, Italy,

Bibliografia

• [1] Bae, K., Meseguer, J.: The Linear Temporal Logic of Rewriting Maude Model Checker, Proceedings of the 8th International Workshop on Rewriting Logic and its Applications (WRLA'10) (P. C. Ölveczky, Ed.), 6381, Springer, 2010, 208-225.
• [2] Balbiani, P., Echahed, R., Herzig, A.: A Dynamic Logic for Termgraph Rewriting, Proceedings of the 5th International Conference on Graph Transformations (ICGT'10) (H. Ehrig, A. Rensink, G. Rozenberg, A. Schürr, Eds.), 6372, Springer, 2010, 59-74.
• [3] Baldan, P., Corradini, A., König, B.: A Static Analysis Technique for Graph Transformation Systems, Proceedings of the 12th InternationalConference on Concurrency Theory (CONCUR'01) (K. Larsen,M. Nielsen, Eds.), 2154, Springer, 2001, 381-395.
• [4] Baldan, P., Corradini, A., König, B., Lluch Lafuente, A.: A Temporal Graph Logic for Verification of Graph Transformation Systems, Proceedings of the 18th International Workshop on Recent Trends in Algebraic Development Techniques (WADT'06) (J. L. Fiadeiro, P.-Y. Schobbens, Eds.), 4409, Springer, 2007, 1-20.
• [5] Belardinelli, F.: QuantifiedModal Logic and the Ontology of PhysicalObjects, Ph.D. Thesis, Scuola Normale Superiore of Pisa, 2006.
• [6] Boneva, I., Rensink, A., Kurban, M., Bauer, J.: Graph Abstraction and Abstract Graph Transformation, Technical Report TR-CTIT-07-50, Centre for Telematics and Information Technology, University of Twente, 2007.
• [7] Boronat, A., Heckel, R., Meseguer, J.: Rewriting Logic Semantics and Verification of Model Transformations, Proceedings of the 12th International Conference on Fundamental Aspects of Software Engineering (FASE'09) (M. Chechik, M. Wirsing, Eds.), 5503, Springer, 2009, 18-33.
• [8] Brochenin, R., Demri, S., Lozes, E.: On the Almighty Wand, Proceedings of the 17th Annual Conference of the EACSL on Computer Science Logic (CSL'08) (M. Kaminski, S. Martini, Eds.), 5213, Springer, 2008, 323-338.
• [9] Brochenin, R., Demri, S., Lozes, E.: Reasoning about Sequences of Memory States, Annals of Pure and Applied Logic, 161(3), 2009, 305-323.
• [10] Caires, L.: Behavioral and Spatial Observations in a Logic for the π-Calculus, Proceedings of the 7th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'04) (I. Walukiewicz, Ed.), 2987, Springer, 2004, 72-87.
• [11] Caires, L., Cardelli, L.: A Spatial Logic for Concurrency (part I), Information and Computation, 186(2), 2003, 194-235.
• [12] Cardelli, L., Gardner, P., Ghelli, G.: A Spatial Logic for Querying Graphs, Proceedings of the 30th International Colloquium on Automata, Languages and Programming (ICALP'02) (P. Widmayer, F. T. Ruiz, R. M. Bueno, M. Hennessy, S. Eidenbenz, R. Conejo, Eds.), 2380, Springer, 2002, 597-610.
• [13] Cardelli, L., Gardner, P., Ghelli, G.: Manipulating Trees with Hidden Labels, Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'03) (A. Gordon, Ed.), 2620, Springer, 2003, 216-232.
• [14] Cardelli, L., Ghelli, G.: TQL: A Query Language for Semistructured Data Based on the Ambient Logic, Mathematical Structures in Computer Science, 14(3), 2004, 285-327.
• [15] Cardelli, L., Gordon, A. D.: Anytime, Anywhere: Modal Logics for Mobile Ambients, Proceedings of the 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00), 2000, 365-377.
• [16] Clavel, M., Durán, F., Eker, S., Lincoln, P., Mart´ı-Oliet, N., Meseguer, J., Talcott, C. L.: All about Maude, vol. 4350 of Lecture Notes in Computer Science, Springer, 2007.
• [17] Conforti, G., Macedonio, D., Sassone, V.: Static BiLog: a Unifying Language for Spatial Structures, Fundamenta Informaticae, 80(1-3), 2007, 91-110.
• [18] Courcelle, B.: The Monadic Second-Order Logic of Graphs, II: Infinite Graphs of Bounded Width, Mathematical Systems Theory, 21(4), 1989, 187-221.
• [19] Courcelle, B.: The Monadic Second-Order Logic of Graphs. I. Recognizable Sets of Finite Graphs, Information and Computation, 85(1), 1990, 12-75.
• [20] Courcelle, B.: The Expression of Graph Properties and Graph Transformations in Monadic Second-Order Logic, in: Handbook of Graph Grammars and Computing by Graph Transformation (G. Rozenberg, Ed.), World Scientific, 1997, 313-400.
• [21] Dawar, A., Gardner, P., Ghelli, G.: Expressiveness and Complexity of Graph Logic, Information and Computation, 205(3), 2007, 263-310.
• [22] Distefano, D., Katoen, J.-P., Rensink, A.: Who is PointingWhen toWhom?, Proceedings of the 32nd International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'04) (K. Lodaya,M. Mahajan, Eds.), 3328, Springer, 2004, 250-262.
• [23] Distefano, D., Rensink, A., Katoen, J.-P.: Model Checking Birth and Death, Procedings of the 2nd IFIP International Conference on Theoretical Computer Science (TCS'02) (R. A. Baeza-Yates, U. Montanari, N. Santoro, Eds.), 223, Kluwer, 2002, 435-447.
• [24] Ferrari, G., Lluch Lafuente, A.: A Logic for Graphs with QoS, Proceedings of the 1st InternationalWorkshop on Views on Designing Complex Architectures (VODCA'04) (F. Gadducci, M. ter Beek, Eds.), 142, Elsevier, 2006, 143-160.
• [25] Franconi, E., Toman, D.: Fixpoint Extensions of Temporal Description Logics, Proceedings of the 16th International Workshop on Description Logics (DL'03) (D. Calvanese, G. D. Giacomo, E. Franconi, Eds.), 81, CEUR-WS.org, 2003.
• [26] Gadducci, F., Lluch Lafuente, A.: Graphical Encoding of a Spatial Logic for the π-Calculus, Proceedings of the 2nd International Conference on Algebra and Coalgebra in Computer Science (CALCO'07) (T. Mossakowski, U. Montanari,M. Haveraaen, Eds.), 4624, Springer, 2007, 209-225.
• [27] Gadducci, F., Lluch Lafuente, A., Vandin, A.: Counterpart Semantics for a Second-Order μ-Calculus, Proceedings of the 5th International Conference on Graph Transformation (ICGT'10) (H. Ehrig, A. Rensink, G. Rozenberg, A. Schürr, Eds.), 6372, Springer, 2010, 282-297.
• [28] Gusfield, D., Irving, R. W.: The Stable Marriage Problem: Structure and Algorithms, MIT Press, 1989.
• [29] Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic, MIT Press, Cambridge, 2000.
• [30] Hazen, A.: Counterpart-Theoretic Semantics for Modal Logic, The Journal of Philosophy, 76(6), 2004, 319-338.
• [31] Hirsch, D., Lluch Lafuente, A., Tuosto, E.: A Logic for Application Level QoS, Proceedings of the 3rd Workshop on Quantitative Aspects of Programming Languages (QAPL'05), 153(2), Elsevier, 2006, 135-159.
• [32] Hodkinson, I.M.,Wolter, F., Zakharyaschev,M.: Monodic Fragments of First-Order Temporal Logics: 2000-2001 A.D, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'01) (R. Nieuwenhuis, A. Voronkov, Eds.), 2250, Springer, 2001, 1-23.
• [33] Leivant, D.: Propositional Dynamic Logic with Program Quantifiers, Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV) (A. Brauer,M.Mislove, Eds.), 218, Elsevier, 2008, 231-240.
• [34] Lluch Lafuente, A.: Towards Model Checking Spatial Properties with SPIN, Proceedings of the 14th International SPIN Workshop on Model Checking Software (SPIN'07) (D. Bosnacki, S. Edelkamp, Eds.), 4595, Springer, 2007, 223-242.
• [35] Lluch Lafuente, A., Meseguer, J., Vandin, A.: State Space C-Reductions of Concurrent Systems in Rewriting Logic, Submitted for publication.
• [36] Lluch Lafuente, A., Vandin, A.: Towards a Maude Tool for Model Checking Temporal Graph Properties, Proceedings of the 10th International Workshop on Graph Transformation and Visual Modelling Languages (GT-VMT'11) (F. Gadducci, L. Mariani, Eds.), 42, EAAST, 2011.
• [37] Lozes, é., Villard, J.: A Spatial Equational Logic for the Applied π-Calculus, Distributed Computing, 23(1), 2010, 61-83.
• [38] Meseguer, J.: The Temporal Logic of Rewriting: A Gentle Introduction, Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday (P. Degano, R. D. Nicola, J. Meseguer, Eds.), 5065, Springer, 2008, 354-382.
• [39] Montanari, U., Pistore, M.: Structured Coalgebras and Minimal HD-Automata for the π-Calculus, Theoretical Computer Science, 340(3), 2005, 539-576.
• [40] Reif, J., Sistla, A. P.: A Multiprocess Network Logic with Temporal and Spatial Modalities, International Journal of Computer and System Sciences, 30(1), 1985, 41-53.
• [41] Rensink, A.: Towards Model Checking Graph Grammars, Proceedings of the 3rd Workshop on Automated Verification of Critical Systems (AVOCS'03) (M. Leuschel, S. Gruner, S. Lo Presti, Eds.), DSSE-TR-2003-2, University of Southampton, 2003, 150-160.
• [42] Rensink, A.: Isomorphism Checking in GROOVE, Proceedings of the International Workshop on Graph Based Tools (GRABATS'06) (A. Zündorf, D. Varró, Eds.), 1, EAAST, 2006.
• [43] Rensink, A.: Model Checking Quantified Computation Tree Logic, Proceedings of the 17th International Conference on Concurrency Theory (CONCUR'06) (C. Baier, H. Hermanns, Eds.), 4137, Springer, 2006, 110-125.
• [44] Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS'02), IEEE Computer Society, 2002, 55-74.
• [45] Yahav, E., Reps, T. W., Sagiv, S., Wilhelm, R.: Verifying Temporal Heap Properties Specified via Evolution Logic, Logic Journal of the IGPL, 14(5), 2006, 755-783