Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Selected publications by Philippe Schnoebelen
[go: Go Back, main page]

  LSV
LSV
Selected publications by
Philippe Schnoebelen

ENS de Cachan
CNRS



2006
C. Baier, N. Bertrand and Ph. SchnoebelenVerifying nondeterministic probabilistic channel systems against ω-regular linear-time propertiesACM Transactions on Computational Logic, 2006. To appear. ( Web page | PDF | PS | BibTeX + Abstract )
C. Baier, N. Bertrand and Ph. SchnoebelenOn Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel SystemsIn Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), Phnom Penh, Cambodia, November 2006, LNAI 4246, pages 347-361. Springer. ( PDF | PS | PS.GZ | BibTeX + Abstract )
C. Baier, N. Bertrand and Ph. SchnoebelenSymbolic verification of communicating systems with probabilistic message losses: liveness and fairnessIn Proceedings of 26th IFIP WG6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'06), Paris, France, September 2006, LNCS 4229, pages 212-227. Springer. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )
A. Kucera and Ph. SchnoebelenA General Approach to Comparing Infinite-State Systems with Their Finite-State SpecificationsTheoretical Computer Science 358(2-3), pages 315-333, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
N. Bertrand and Ph. SchnoebelenA short visit to the STS hierarchyIn Proceedings of the 12th International Workshop on Expressiveness in Concurrency (EXPRESS'05), San Francisco, CA, USA, August 2005, ENTCS 154(3), pages 59-69. Elsevier Science Publishers, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
A. Rabinovich and Ph. SchnoebelenBTL2 and the expressive power of ECTL+Information and Computation 204(7), pages 1023-1044, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
S. Demri, F. Laroussinie and Ph. SchnoebelenA Parametric Analysis of the State Explosion Problem in Model CheckingJournal of Computer and System Sciences 72(4), pages 547-575, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
F. Laroussinie, N. Markey and Ph. SchnoebelenEfficient Timed Model Checking for Discrete-Time SystemsTheoretical Computer Science 353(1-3), pages 249-271, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
N. Markey and Ph. SchnoebelenMu-Calculus Path CheckingInformation Processing Letters 97(6), pages 225-230, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
C. Baier, N. Bertrand and Ph. SchnoebelenA note on the attractor-property of infinite-state Markov chainsInformation Processing Letters 97(2), pages 58-63, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
2005
B. Bouyssonouse and J. Sifakis (eds.).  Embedded Systems Design: The ARTIST Roadmap for Research and Development, LNCS 3436. Springer, 2005. ( Web page | BibTeX )
P. A. Abdulla, N. Bertrand, A. Rabinovich and Ph. SchnoebelenVerification of Probabilistic Systems with Faulty CommunicationInformation and Computation 202(2), pages 141-165, 2005. ( PDF | PS | PS.GZ | BibTeX + Abstract )
D. Lugiez and Ph. SchnoebelenDecidable first-order transition logics for PA-processesInformation and Computation 203(1), pages 75-113, 2005. ( PDF | PS | PS.GZ | BibTeX + Abstract )
S. Bardin, A. Finkel, J. Leroux and Ph. SchnoebelenFlat acceleration in symbolic model checkingIn Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), Taipei, Taiwan, ROC, October 2005, LNCS 3707, pages 474-488. Springer. ( PDF | PS | PS.GZ | BibTeX + Abstract )
2004
Ph. SchnoebelenThe Verification of Probabilistic Lossy Channel SystemsIn Validation of Stochastic Systems: A Guide to Current Research, LNCS 2925, pages 445-465. Springer, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract )
N. Markey and Ph. SchnoebelenSymbolic Model Checking of Simply-Timed SystemsIn Proceedings of the Joint Conferences Formal Modelling and Analysis of Timed Systems (FORMATS'04) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'04), Grenoble, France, September 2004, LNCS 3253, pages 102-117. Springer. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
N. Markey and Ph. SchnoebelenTSMV: A Symbolic Model Checker for Quantitative Analysis of SystemsIn Proceedings of the 1st International Conference on Quantitative Evaluation of Systems (QEST'04), Enschede, The Netherlands, September 2004, pages 330-331. IEEE Computer Society Press. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
A. Kucera and Ph. SchnoebelenA General Approach to Comparing Infinite-State Systems with Their Finite-State SpecificationsIn Proceedings of the 15th International Conference on Concurrency Theory (CONCUR'04), London, UK, August 2004, LNCS 3170, pages 372-386. Springer. ( PDF | BibTeX + Abstract )
F. Laroussinie, N. Markey and Ph. SchnoebelenModel Checking Timed Automata with One or Two ClocksIn Proceedings of the 15th International Conference on Concurrency Theory (CONCUR'04), London, UK, August 2004, LNCS 3170, pages 387-401. Springer. ( PDF | PS | PS.GZ | BibTeX + Abstract )
Ph. Schnoebelen (ed.).  Proceedings of the 5th International Workshop on Verification of Infinite State Systems (INFINITY'03), Marseilles, France, September 2003, ENTCS 98. Elsevier Science Publishers, 2004. ( Web page | BibTeX )
N. Bertrand and Ph. SchnoebelenVerifying Nondeterministic Channel Systems With Probabilistic Message LossesIn Proceedings of the 3rd International Workshop on Automated Verification of Infinite-State Systems (AVIS'04), Barcelona, Spain, April 2004. ( PDF | BibTeX + Abstract )
N. Markey and Ph. SchnoebelenA PTIME-Complete Matching Problem for SLP-Compressed WordsInformation Processing Letters 90(1), pages 3-6, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract )
2003
Ph. SchnoebelenThe Complexity of Temporal Logic Model CheckingIn Selected Papers from the 4th Workshop on Advances in Modal Logics (AiML'02), Toulouse, France, September 2002, pages 393-436. King's College Publication, 2003. Invited paper. ( PDF | PS | PS.GZ | BibTeX )
N. Markey and Ph. SchnoebelenModel Checking a Path (Preliminary Report)In Proceedings of the 14th International Conference on Concurrency Theory (CONCUR'03), Marseilles, France, August 2003, LNCS 2761, pages 251-265. Springer. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
Ph. SchnoebelenOracle circuits for branching-time model checkingIn Proceedings of the 30th International Colloquium on Automata, Languages and Programming (ICALP'03), Eindhoven, The Netherlands, June 2003, LNCS 2719, pages 790-801. Springer. ( PDF | PS | PS.GZ | BibTeX + Abstract )
N. Bertrand and Ph. SchnoebelenModel Checking Lossy Channels Systems Is Probably DecidableIn Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'03), Warsaw, Poland, April 2003, LNCS 2620, pages 120-135. Springer. ( PDF | PS | PS.GZ | BibTeX + Abstract )
F. Laroussinie, Ph. Schnoebelen and M. TuruaniOn the Expressivity and Complexity of Quantitative Branching-Time Temporal LogicsTheoretical Computer Science 297(1-3), pages 297-315, 2003. ( PS | PS.GZ | BibTeX + Abstract )
2002
S. Hornus and Ph. SchnoebelenOn Solving Temporal Logic QueriesIn Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology (AMAST'02), Saint Gilles les Bains, Reunion Island, France, September 2002, LNCS 2422, pages 163-177. Springer. ( PDF | PS | PS.GZ | BibTeX + Abstract )
Ph. SchnoebelenVerifying Lossy Channel Systems has Nonprimitive Recursive ComplexityInformation Processing Letters 83(5), pages 251-261, 2002. ( PDF | PS | PS.GZ | BibTeX + Abstract )
B. Masson and Ph. SchnoebelenOn Verifying Fair Lossy Channel SystemsIn Proceedings of the 27th International Symposium on Mathematical Fundations of Computer Science (MFCS'02), Warsaw, Poland, August 2002, LNCS 2420, pages 543-555. Springer. ( PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )
A. Labroue and Ph. SchnoebelenAn Automata-Theoretic Approach to the Reachability Analysis of RPPS SystemsNordic Journal of Computing 9(2), pages 118-144, 2002. ( PS | PS.GZ | BibTeX + Abstract )
F. Laroussinie, N. Markey and Ph. SchnoebelenTemporal Logic with Forgettable PastIn Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), Copenhagen, Denmark, July 2002, pages 383-392. IEEE Computer Society Press. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
S. Demri and Ph. SchnoebelenThe Complexity of Propositional Linear Temporal Logics in Simple CasesInformation and Computation 174(1), pages 84-103, 2002. ( PDF | PS | PS.GZ | BibTeX + Abstract )
F. Laroussinie, N. Markey and Ph. SchnoebelenOn Model Checking Durational Kripke Structures (Extended Abstract)In Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'02), Grenoble, France, April 2002, LNCS 2303, pages 264-279. Springer. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
S. Demri, F. Laroussinie and Ph. SchnoebelenA Parametric Analysis of the State Explosion Problem in Model Checking (Extended Abstract)In Proceedings of the 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS'02), Antibes Juan-les-Pins, France, March 2002, LNCS 2285, pages 620-631. Springer. ( PDF | PS | PS.GZ | BibTeX + Abstract )
D. Lugiez and Ph. SchnoebelenThe Regular Viewpoint on PA-ProcessesTheoretical Computer Science 274(1-2), pages 89-115, 2002. ( PDF | PS | PS.GZ | BibTeX + Abstract )
2001
B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci and Ph. SchnoebelenSystems and Software Verification. Model-Checking Techniques and Tools. Springer, 2001. ( Web page | BibTeX )
Ph. SchnoebelenBisimulation and Other Undecidable Equivalences for Lossy Channel SystemsIn Proceedings of the 4th International Workshop on Theoretical Aspects of Computer Software (TACS'01), Sendai, Japan, October 2001, LNCS 2215, pages 385-399. Springer. ( PDF | PS | PS.GZ | BibTeX + Abstract )
Ph. SchnoebelenSpécification et vérification des systèmes concurrents.  Mémoire d'habilitation, Université Paris 7, Paris, France, October 2001. ( PS | PS.GZ | BibTeX )
A. Finkel and Ph. SchnoebelenWell-Structured Transition Systems Everywhere!  Theoretical Computer Science 256(1-2), pages 63-92, 2001. ( PDF | PS | PS.GZ | BibTeX + Abstract )
F. Laroussinie, N. Markey and Ph. SchnoebelenModel checking CTL+ and FCTL is hardIn Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'01), Genova, Italy, April 2001, LNCS 2030, pages 318-331. Springer. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
2000
I. A. Lomazova and Ph. SchnoebelenSome Decidability Results for Nested Petri NetsIn Proceedings of the 3rd International Andrei Ershov Memorial Conference on Perspectives of System Informatics (PSI'99), Novosibirsk, Russia, July 1999, LNCS 1755, pages 208-220. Springer, 2000. ( PS | PS.GZ | BibTeX )
G. Canet, S. Couffin, J.-J. Lesage, A. Petit and Ph. SchnoebelenTowards the Automatic Verification of PLC Programs Written in Instruction ListIn Proceedings of the IEEE International Conference on Systems, Man and Cybernetics (SMC 2000), Nashville, Tennessee, USA, October 2000, pages 2449-2454. Argos Press. ( PS | PS.GZ | BibTeX + Abstract )
O. De Smet, S. Couffin, O. Rossi, G. Canet, J.-J. Lesage, Ph. Schnoebelen and H. Papini.  Safe Programming of PLC Using Formal Verification MethodsIn Proceedings of the 4th International PLCopen Conference on Industrial Control Programming (ICP 2000), Utrecht, The Netherlands, October 2000, pages 73-78. PLCopen. ( PS | PS.GZ | BibTeX )
O. Rossi and Ph. SchnoebelenFormal modeling of timed function blocks for the automatic verification of Ladder Diagram programsIn Proceedings of the 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems (ADPM 2000), Dortmund, Germany, September 2000, pages 177-182. Shaker Verlag. ( PS | PS.GZ | BibTeX )
G. Canet, B. Denis, A. Petit, O. Rossi and Ph. SchnoebelenUn cadre pour la vérification automatique de programmes ILIn Actes de la 1ère Conférence Internationale Francophone d'Automatique (CIFA 2000), Lille, France, July 2000, pages 693-698. Union des Chercheurs Ingénieurs et Scientifiques, Villeneuve d'Ascq, France. ( PS | PS.GZ | BibTeX )
D. Lugiez and Ph. SchnoebelenDecidable First-Order Transition Logics for PA-ProcessesIn Proceedings of the 27th International Colloquium on Automata, Languages and Programming (ICALP 2000), Geneva, Switzerland, July 2000, LNCS 1853, pages 342-353. Springer. ( PS | PS.GZ | BibTeX )
Ph. Schnoebelen and N. SidorovaBisimulation and the Reduction of Petri NetsIn Proceedings of the 21st International Conference on Applications and Theory of Petri Nets (ICATPN 2000), AArhus, Denmark, June 2000, LNCS 1825, pages 409-423. Springer. ( PS | PS.GZ | BibTeX )
B. Bérard, A. Labroue and Ph. SchnoebelenVerifying Performance Equivalence for Timed Basic Parallel ProcessesIn Proceedings of the 3rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2000), Berlin, Germany, March 2000, LNCS 1784, pages 35-47. Springer. ( PS | PS.GZ | BibTeX )
F. Laroussinie and Ph. SchnoebelenThe State-Explosion Problem from Trace to Bisimulation EquivalenceIn Proceedings of the 3rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2000), Berlin, Germany, March 2000, LNCS 1784, pages 192-207. Springer. ( PS | PS.GZ | BibTeX )
F. Laroussinie and Ph. SchnoebelenSpecification in CTL+Past for verification in CTLInformation and Computation 156(1-2), pages 236-263, 2000. ( PS | PS.GZ | BibTeX )
1999
C. Dufourd, P. Jancar and Ph. SchnoebelenBoundedness of Reset P/T NetsIn Proceedings of the 26th International Colloquium on Automata, Languages and Programming (ICALP'99), Prague, Czech Republic, July 1999, LNCS 1644, pages 301-310. Springer. ( PS | PS.GZ | BibTeX + Abstract )
Ph. Schnoebelen, B. Bérard, M. Bidoit, F. Laroussinie and A. PetitVérification de logiciels : techniques et outils du model-checking. Vuibert, 1999. ( Web page | BibTeX )
Ph. SchnoebelenDecomposable Regular Languages and the Shuffle OperatorEATCS Bulletin 67, pages 283-289, 1999. ( PS | PS.GZ | BibTeX )
1998
C. Dufourd, A. Finkel and Ph. SchnoebelenReset Nets between Decidability and UndecidabilityIn Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP'98), Aalborg, Denmark, July 1998, LNCS 1443, pages 103-115. Springer. ( PS | PS.GZ | BibTeX + Abstract )
A. Finkel and Ph. SchnoebelenFundamental Structures in Well-Structured Infinite Transition SystemsIn Proceedings of the 3rd Latin American Symposium on Theoretical Informatics (LATIN'98), Campinas, Brasil, April 1998, LNCS 1380, pages 102-118. Springer. ( PS | PS.GZ | BibTeX )
1997
O. Kouchnarenko and Ph. SchnoebelenA Model for Recursive-Parallel ProgramsIn Proceedings of the 1st International Workshop on Verification of Infinite State Systems (INFINITY'96), Pisa, Italy, August 1996, ENTCS 5, page 30. Elsevier Science Publishers, 1997. ( PS | PS.GZ | BibTeX )
O. Kouchnarenko and Ph. SchnoebelenA Formal Framework for the Analysis of Recursive-Parallel ProgramsIn Proceedings of the 4th International Conference on Parallel Computing Technologies (PaCT'97), Yaroslavl, Russia, September 1997, LNCS 1277, pages 45-59. Springer. ( PS | PS.GZ | BibTeX )
1996
O. Kouchnarenko and Ph. SchnoebelenModèles formels pour les programmes récursifs-parallèlesIn Actes des 8èmes Rencontres Francophones du Parallélisme (RENPAR'96), Bordeaux, France, May 1996, pages 85-88. ( PS | PS.GZ | BibTeX )
1995
F. Laroussinie and Ph. SchnoebelenA Hierarchy of Temporal Logics with PastTheoretical Computer Science 148(2), pages 303-324, 1995. ( PS | PS.GZ | BibTeX )
F. Laroussinie, S. Pinchinat and Ph. SchnoebelenTranslations between Modal Logics of Reactive SystemsTheoretical Computer Science 140(1), pages 53-71, 1995. ( PS | PS.GZ | BibTeX )
1994
F. Laroussinie, S. Pinchinat and Ph. SchnoebelenTranslation Results for Modal Logics of Reactive SystemsIn Proceedings of the 3rd International Conference on Algebraic Methodology and Software Technology (AMAST'93), Twente, The Netherlands, June 1993, Workshops in Computing, pages 299-310. Springer-Verlag, 1994. ( BibTeX )
C. Autant, W. Pfister and Ph. SchnoebelenPlace Bisimulations for the Reduction of Labeled Petri Nets with Silent MovesIn Proceedings of the 6th International Conference on Computing and Information (ICCI'94), Peterborough, Ontario, Canada, May 1994, pages 230-246. ( PS | PS.GZ | BibTeX )
S. Pinchinat, F. Laroussinie and Ph. SchnoebelenLogical Characterizations of Truly Concurrent Bisimulation.  Technical Report 114, Laboratoire d'Informatique Fondamentale et d'Intelligence Artificielle, Grenoble, France, March 1994. ( PS | PS.GZ | BibTeX )
F. Laroussinie and Ph. SchnoebelenA Hierarchy of Temporal Logics with PastIn Proceedings of the 11th Annual Symposium on Theoretical Aspects of Computer Science (STACS'94), Caen, France, February 1994, LNCS 775, pages 47-58. Springer-Verlag. ( BibTeX )
1992
C. Autant and Ph. SchnoebelenPlace Bisimulations in Petri NetsIn Proceedings of the 13th International Conference on Applications and Theory of Petri Nets (APN'92), Sheffield, UK, June 1992, LNCS 616, pages 45-61. Springer-Verlag. ( BibTeX )
1991
F. Cherief and Ph. Schnoebelenτ-Bisimulations and Full Abstraction for Refinement of ActionsInformation Processing Letters 40(4), pages 219-222, 1991. ( BibTeX )
Ph. SchnoebelenExperiments on Processes with BacktrackingIn Proceedings of the 2nd International Conference on Concurrency Theory (CONCUR'91), Amsterdam, The Netherlands, August 1991, LNCS 527, pages 480-494. Springer-Verlag. ( BibTeX )
C. Autant, Z. Belmesk and Ph. SchnoebelenStrong Bisimilarity on Nets RevisitedIn Proceedings of the 3rd International Conference Parallel Architectures and Languages Europe (PARLE'91), Volume II: Parallel Languages, Eindhoven, The Netherlands, June 1991, LNCS 506, pages 295-312. Springer-Verlag. ( BibTeX )
H. Comon, D. Lugiez and Ph. SchnoebelenA Rewrite-Based Type Discipline for a Subset of Computer AlgebraJournal of Symbolic Computation 11(4), pages 349-368, 1991. ( BibTeX )
1990
C. Autant, Z. Belmesk and Ph. SchnoebelenA Net-Theoretic Approach to the Efficient Implementation of the FP2 Parallel LanguageIn Proceedings of the 11th International Conference on Applications and Theory of Petri Nets (APN'90), Paris, France, June 1990, pages 451-470. ( BibTeX )
Ph. SchnoebelenSémantique du parallélisme et logique temporelle. Application au langage FP2.  Thèse de doctorat, Institut National Polytechnique de Grenoble, France, June 1990. ( BibTeX )
Ph. Schnoebelen and S. PinchinatOn the Weak Adequacy of Branching-Time Temporal LogicIn Proceedings of the 3rd European Symposium on Programming (ESOP'90), Copenhagen, Denmark, May 1990, LNCS 432, pages 377-388. Springer-Verlag. ( BibTeX )
1989
Ph. Schnoebelen and Ph. Jorrand.  Principles of FP2: Term Algebras for Specification of Parallel MachinesIn Languages for Parallel Architectures: Design, Semantics, Implementation Models, chapter 5, pages 223-273. Wiley, 1989. ( BibTeX )
1988
Ph. SchnoebelenRefined Compilation of Pattern-Matching for Functional LanguagesScience of Computer Programming 11(2), pages 133-159, 1988. ( BibTeX )
Ph. SchnoebelenRefined Compilation of Pattern-Matching for Functional LanguagesIn Proceedings of the 1st International Workshop on Algebraic and Logic Programming (ALP'88), Gaussig, German Democratic Republic, November 1988, LNCS 343, pages 233-243. Springer-Verlag. ( BibTeX )
1987
P. Schäfer and Ph. SchnoebelenSpecification of a Pipelined Event-Driven Simulator Using FP2In Proceedings of the 1st International Conference Parallel Architectures and Languages Europe (PARLE'87), Volume I: Parallel Architectures, Eindhoven, The Netherlands, June 1987, LNCS 258, pages 311-328. Springer-Verlag. ( BibTeX )
Ph. SchnoebelenRewriting Techniques for the Temporal Analysis of Communicating ProcessesIn Proceedings of the 1st International Conference Parallel Architectures and Languages Europe (PARLE'87), Volume II: Parallel Languages, Eindhoven, The Netherlands, June 1987, LNCS 259, pages 402-419. Springer-Verlag. ( BibTeX )
Page maintenue par Nicolas Markey.  Dernières modifications : le 22 novembre 2006
Valid HTML 4.01!