Margherita Napoli , Selected Publications

• A NuSMV Extension for Graded-CTL Model Checking. In CAV 2010, Edinburgh, UK, July 15-19, 2010 Lecture Notes in Computer Science. (to appear).
  (with A. Ferrante, M. Memoli, M. Parente, and F. Sorrentino)
• Graded Alternating-Time Temporal Logic. In: LPAR 2010. Dakar, Senagal, 25/05/2010-01/06/2010.
  (with M. Faella and M. Parente)
• Parametric Metric Interval Temporal Logic. In LATA 2010, Trier, Germany, May 24-28, 2010 Lecture Notes in Computer Science. (to appear).
  (with B. Di Giampaolo and S. La Torre)
• Model-Checking for Graded CTL. FUNDAMENTA INFORMATICAE, vol. 96(3); p. 323-339; (2009).
  (with A. Ferrante and M. Parente.)
• Graded Alternating-time temporal logc. In: 24-esimo Convegno Italiano di Logica Computazionale. Ferrara, giugno 2009: Marco Gavanelli and Fabrizio Riguzzi, CILC 2009, p. 1-15; (2009).
  (with M. Faella and M. Parente)
• Graded-CTL: Satisfiability and Symbolic Model Checking. In: 11th International Conference on Formal Engineering Methods ICFEM'09, Rio de Janeiro, Brazil, December 9-12, 2009 Lecture Notes in Computer Science, Springer-Verlag, vol. 5885, p. 306-325 (2009).
  (with A. Ferrante and M. Parente.)
• CTL Model-Checking with Graded Quantifiers. In:6th International Symposium on Automated Technology for Verification and Analysis October 20-23, 2008, Seoul, Korea Lecture Notes in Computer Science, Springer-Verlag, vol. 5311, p. 18-32 (2008).
  (with A. Ferrante and M. Parente)
• Program Complexity in Hierarchical Module Checking. In: LPAR 2008, Doha, Qatar, 22/11/2008-27/11/2008, Lecture Notes in Computer Science, Springer-Verlag, vol. 5330 p. 318-332; (2008).
  (with A. Murano and M. Parente)
• Graded CTL Model-Checking. In: 23-esimo Convegno Italiano di Logica Computazionale. Perugia, 10-12 luglio 2008; Perugia, CILC 2008, p. 1-15; (2008).
  (with A. Ferrante and M. Parente)
• Verification of Scope-dependent Hierarchical State Machines. INFORMATION AND COMPUTATION, vol. 206; p. 1161-1177; (2008).
  (with S. La Torre, M. Parente, and G. Parlato)
• The word problem for visibly pushdown languages described by grammars. FORMAL METHODS IN SYSTEM DESIGN, vol. 31; p. 265-279; (2007).
  (with S. La Torre and M. Parente)
• Verification of Succinct Hierarchical State Machine. In: 1st International Conference on Language and Automata Theory and Applications. Tarragona, Spain, 29/03/2007 - 04/04/2007, TARRAGONA: Universitat Rovira i Virgili, LATA 2007, p. 485-496; (2007).
  (with S. La Torre, M. Parente, and G. Parlato)
• On the Membership Problem for Visibly Pushdown Languages. In: Proc. of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA 2006). Lecture Notes in Computer Science. Bejing, China, 23-26 Ottobre 2006, BERLIN: SPRINGER, vol. 4218, p. 96-109; (2006).
  (with S. La Torre and M. Parente)
• Different Time Solutions for the Firing Squad Synchronization Problem on Basic Grid Networks. RAIRO THEORETICAL INFORMATICS AND APPLICATIONS, vol. 40(2); p. 177-206; (2006).
  (with J. Gruska, S. La Torre and M. Parente)
• Weak Muller acceptance conditions for tree automata. THEORETICAL COMPUTER SCIENCE, vol.332(1-3); p. 233-250 (2005)
  (with S. La Torre and A. Murano)
• Finite automata on timed omega-trees. THEORETICAL COMPUTER SCIENCE, vol.293 (3); p. 479-505 (2003)
  (with S. La Torre)
• Specification and Verification of Protocols With Time Constraints. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, vol. 99; p. 205-227; (2004).
  (with M. Parente and A. Peron)
• Hierarchical and Recursive State Machine with Context-Dependent Properties. In: Automata, Languages and Programming. Eindhoven, The Netherlands, June 30 - July 4, 2003, vol. LNCS 2719, ICALP 2003 p. 776-789; (2003).
  (with S. La Torre, M. Parente, and G. Parlato)
• Firing Squad Synchronization Problem on Bidimensional Cellular Automata with Communication Constraints. In: Universal Machines and Computations. Chisinau, Moldavia, Maggio 2001, vol. LNCS 2005, MCU 2001 p. 264-275; (2001).
  (with S. La Torre and M. Parente)
• Compositionality in the Synchronization of Processors Exchanging a minimal amount of Information. In: Proceedings of 5th WSDAAL, 18-20 Settembre, Ischia, Italia, p. 1-10; (2000).
  (with S. La Torre and M. Parente)
• A Compositional Approach to Synchronize Two Dimensional Networks of Processor. RAIRO. THEORETICAL INFORMATICS AND APPLICATIONS, vol. 34(6); p. 549-564; (2000).
  (with S. La Torre and M. Parente)
• Weak Muller Acceptance Conditions for Tree Automata Proc. of the 3rd International Workshop on Verification, Model Checking, and Abstract Interpretation, VMCAI'02, Venezia, Italy, January 21 - 22, 2002. Springer-Verlag, LNCS. 2055, 264 - 275.
  (with S. La Torre and A. Murano)
• Timed Tree Automata with an Application to Temporal Logic ACTA INFORMATICA vol. 38(2), p. 89 - 116, 2001.
  (with S. La Torre)
• Automata-based Representations for Infinite Graphs RAIRO. THEORETICAL INFORMATICS AND APPLICATIONS, vol. 35(4), 311 - 330, 2001.
  (with S. La Torre)
• Firing Squad Synchronization Problem on Bidimensional Cellular Automata with Communication Constraint Proc. of the 3rd International Conference on Machines, Computations and Universality, MCU'2001, Chisinau, Moldova, May 23-27, 2001. Springer-Verlag, LNCS 2055, 264 - 275.
  (with S. La Torre and M. Parente)
• A Model of Finite Automata on Timed omega-trees Proc. of the 7th Computing: The Australasian Theory Symposium, CATS'01, Gold Coast, Queensland, Australia, January 29-February 2, 2001. Elsevier Science, ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, vol. 42
  (with S. La Torre)
• A Compositional Approach to Synchronize Two Dimensional Networks of Processors THEORETICAL INFORMATICS AND APPLICATIONS, vol. 34(6),p. 549 - 564, 2000.
  (with S. La Torre and M. Parente)
• A Decidable Dense Branching-time Temporal Logic, Proc. of the 20th Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS'00, New Delhi, India, December 13-15, 2000. Springer-Verlag.
  (with S. La Torre)
• Compositionality in the Synchronization of Processors exchanging a minimal amount of information, Proc. of the 5th Workshop su Sistemi Distribuiti: Algoritmi, Architetture e Linguaggi WSDAAL'00, Ischia, Italy, September 18-20, 2000.
  (with S. La Torre and M. Parente)
• "Representing hyper-graphs by regular languages", Proc of 23rd International Symposium on Mathematical Foundations of Computer Science, Brno, Czech Republic, August 24-28, 1998.L.N.C.S. 1450.
  (with S. La Torre)
• "Synchronization of a line of identical processors at a given time" Fundamenta Informaticae 34(1,2), 103--128, 1998.
  An extended abstract of this paper appeared in the Proc. of the Colloquium on Trees in Algebra and Programming, CAAP '97, in the framework of the Seventh International Joint Conference on the Theory and Practice of Software Development, TAPSOFT'97, Lille, France, April 14 - 18, 1997. L.N.C.S. 1214, 405--416.
  (with S. La Torre and M. Parente)
• "Synchronization of 1-way connected processors" COMPLEX SYSTEMS vol. 10(4), p.239--255, (1998).
  An extended abstract of this paper appeared in the Proc. of the 11-th International Symposium on Fundamentals of Computation Theory, FCT '97, Krakow, Poland, September 1--3, 1997. L.N.C.S. 1279, 293--304.
  (with S. La Torre and M. Parente)
• Parallel Word Substitution, FUNDAMENTA INFORMATICAE vol. 27(1), p. 27--36, 1997.
  (with S. La Torre and M. Parente)
• Succinctness of Description of SBTA Languages, THEORETICAL COMPUTER SCIENCE, vol.179(2), p. 251-271, 1997.
  A preliminary version appeared in the Proc. of the 2-nd LATIN '95, 1995, L.N.C.S. vol. 911, p.346--357, 1995.
  (with J. Gruska, A. Monti and M. Parente)
• Power of Interconnection and of Nondeterminism in Regular Y-Tree Systolic Automata, MATHEMATICAL SYSTEM THEORY vol. 28(3), p.245--266, 1995.
  (with E. Fachini, J. Gruska and M. Parente)
• Optimization of Systolic Tree Automata Proc. of the 13th World Computer Congress, IFIP '94, 1994, Vol.1, 247--252. (North-Holland) Elsevier Science B.V., 1994.
  (with J. Gruska and M. Parente)
• Normal Forms and Nondeterminism in Y-Tree Systolic Automata, Proc. of the 2nd International Colloquium on Words, Languages and Combinatorics, 144--155. World Scientific Publishing Company, 1992.
  (with E. Fachini, J. Gruska, and M. Parente)
• Languages Accepted by Systolic Y-Tree Automata: Structural Characterization. ACTA INFORMATICA, vol. 29(8), p. 143--155, 1992.
  (with E. Fachini, A. Monti and M. Parente)
• The Software Development Workbench WSDW. in Procs. of 4th Int. Conf. on Software Engineering and Knowledge Engineering, Capri, Italy, June 15-20, 1992, pp. 213-221, IEEE Computer Society Press.
  (with A. De Lucia, A. Imperatore, G. Tortora and M. Tucci)
• Systolic Y-Tree Automata: Closure Properties and Decision Problems, Proc. of the 8th International Conference, Fundamentals of Computation Theory, FCT '91, Gosen, Germany, September 9--13, 1991, L.N.C.S. 529, p. 210--219. (with E. Fachini, A. Monti and M. Parente)
• Proving Programs by Queries. in Procs. of 3-th Int. Conf. on Software Engineering and Knowledge Engineering, Skokie, Illinois, USA, June 26-29, 1991, pp. 141-148.
  (with V. De Leo, G. Nota and G. Tortora)
• Systolic Automata on BC-Tree: Characterization and Properties, JOURNAL OF COMPUTERS AND ARTIFICIAL INTELLIGENCE, vol. 8(1), p. 53--82, 1989.
  (with E. Fachini, R. Francese and M. Parente)
• Web, structures: a Tool for Representing and Manipulating Programs., IEEE TRANS. ON SOFT. ENG. vol. 14(11), p. 1597--1609, 1988.
  (with A. Maggiolo Schettini and G. Tortora)
• C-Tree Systolic Automata., THEORETICAL COMPUTER SCIENCE, vol. 56,p. 155--186, 1988. (with E. Fachini)

  ---

  
  
  Dipartimento di Informatica ed Applicazioni "Renato M.Capocelli", Università di Salerno (Italy)