Selected publications by Philippe Schnoebelen

2010
P. Chambart and Ph. SchnoebelenToward a compositional theory of leftist grammars and transformationsIn FoSSaCS'10, LNCS 6014, pages 237-251. Springer, 2010. ( PDF | BibTeX + Abstract )
2008
P. Chambart and Ph. SchnoebelenMixing Lossy and Perfect Fifo ChannelsIn CONCUR'08, LNCS 5201, pages 340-355. Springer, 2008. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )
P. Chambart and Ph. SchnoebelenThe Ordinal Recursive Complexity of Lossy Channel SystemsIn LICS'08, pages 205-216. IEEE Computer Society Press, 2008. ( PDF | BibTeX + Abstract )
P. Chambart and Ph. SchnoebelenThe ω-Regular Post Embedding ProblemIn FoSSaCS'08, LNCS 4962, pages 97-111. Springer, 2008. ( PDF | PS | PS.GZ | BibTeX + Abstract )
P. Bouyer, N. Markey, J. Ouaknine, Ph. Schnoebelen and J. WorrellOn Termination for Faulty Channel MachinesIn STACS'08, Leibniz International Proceedings in Informatics 1, pages 121-132. Leibniz-Zentrum für Informatik, 2008. ( PDF | PS | PS.GZ | BibTeX + Abstract )
2007
C. Baier, N. Bertrand and Ph. SchnoebelenVerifying nondeterministic probabilistic channel systems against ω-regular linear-time propertiesACM Transactions on Computational Logic 9(1), 2007. ( Web page | PDF | PS | BibTeX + Abstract )
P. Chambart and Ph. SchnoebelenPost Embedding Problem is not Primitive Recursive, with Applications to Channel SystemsIn FSTTCS'07, LNCS 4855, pages 265-276. Springer, 2007. ( PDF | PS | PS.GZ | PDF (long version) | BibTeX + Abstract )
Ph. SchnoebelenModel Checking Branching-Time LogicsIn TIME'07, page 5. IEEE Computer Society Press, 2007. ( PDF | PS | PS.GZ | Slides | BibTeX )
2006
C. Baier, N. Bertrand and Ph. SchnoebelenOn Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel SystemsIn LPAR'06, LNAI 4246, pages 347-361. Springer, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
C. Baier, N. Bertrand and Ph. SchnoebelenSymbolic verification of communicating systems with probabilistic message losses: liveness and fairnessIn FORTE'06, LNCS 4229, pages 212-227. Springer, 2006. ( 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 EXPRESS'05, 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 ATVA'05, LNCS 3707, pages 474-488. Springer, 2005. ( PDF | PS | PS.GZ | BibTeX + Abstract )
2004
Ph. SchnoebelenThe Verification of Probabilistic Lossy Channel SystemsIn Validation of Stochastic Systems, LNCS 2925, pages 445-465. Springer, 2004. ( PDF | PS | PS.GZ | BibTeX + Abstract )
N. Markey and Ph. SchnoebelenSymbolic Model Checking for Simply-Timed SystemsIn FORMATS'04/FTRTFT'04, LNCS 3253, pages 102-117. Springer, 2004. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
N. Markey and Ph. SchnoebelenTSMV: A Symbolic Model Checker for Quantitative Analysis of SystemsIn QEST'04, pages 330-331. IEEE Computer Society Press, 2004. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
A. Kucera and Ph. SchnoebelenA General Approach to Comparing Infinite-State Systems with Their Finite-State SpecificationsIn CONCUR'04, LNCS 3170, pages 372-386. Springer, 2004. ( PDF | BibTeX + Abstract )
F. Laroussinie, N. Markey and Ph. SchnoebelenModel Checking Timed Automata with One or Two ClocksIn CONCUR'04, LNCS 3170, pages 387-401. Springer, 2004. ( 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. ( BibTeX )
N. Bertrand and Ph. SchnoebelenVerifying Nondeterministic Channel Systems With Probabilistic Message LossesIn AVIS'04. 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 AiML'02, 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 CONCUR'03, LNCS 2761, pages 251-265. Springer, 2003. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
Ph. SchnoebelenOracle circuits for branching-time model checkingIn ICALP'03, LNCS 2719, pages 790-801. Springer, 2003. ( PDF | PS | PS.GZ | BibTeX + Abstract )
N. Bertrand and Ph. SchnoebelenModel Checking Lossy Channels Systems Is Probably DecidableIn FoSSaCS'03, LNCS 2620, pages 120-135. Springer, 2003. ( 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 AMAST'02, LNCS 2422, pages 163-177. Springer, 2002. ( 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 MFCS'02, LNCS 2420, pages 543-555. Springer, 2002. ( 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 LICS'02, pages 383-392. IEEE Computer Society Press, 2002. ( 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 FoSSaCS'02, LNCS 2303, pages 264-279. Springer, 2002. ( 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 STACS'02, LNCS 2285, pages 620-631. Springer, 2002. ( 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 TACS'01, LNCS 2215, pages 385-399. Springer, 2001. ( 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 FoSSaCS'01, LNCS 2030, pages 318-331. Springer, 2001. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
2000
I. A. Lomazova and Ph. SchnoebelenSome Decidability Results for Nested Petri NetsIn PSI'99, 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 SMC 2000, pages 2449-2454. Argos Press, 2000. ( PS | PS.GZ | BibTeX + Abstract )
O. De Smet, S. Couffin, O. Rossi, G. Canet, J.-J. Lesage, Ph. Schnoebelen and H. PapiniSafe Programming of PLC Using Formal Verification MethodsIn ICP 2000, pages 73-78. PLCopen, 2000. ( PS | PS.GZ | BibTeX )
O. Rossi and Ph. SchnoebelenFormal modeling of timed function blocks for the automatic verification of Ladder Diagram programsIn ADPM 2000, pages 177-182. Shaker Verlag, 2000. ( PS | PS.GZ | BibTeX )
G. Canet, B. Denis, A. Petit, O. Rossi and Ph. SchnoebelenUn cadre pour la vérification automatique de programmes ILIn CIFA 2000, pages 693-698. Union des Chercheurs Ingénieurs et Scientifiques, Villeneuve d'Ascq, France, 2000. ( PS | PS.GZ | BibTeX )
D. Lugiez and Ph. SchnoebelenDecidable First-Order Transition Logics for PA-ProcessesIn ICALP 2000, LNCS 1853, pages 342-353. Springer, 2000. ( PS | PS.GZ | BibTeX )
Ph. Schnoebelen and N. SidorovaBisimulation and the Reduction of Petri NetsIn ICATPN 2000, LNCS 1825, pages 409-423. Springer, 2000. ( PS | PS.GZ | BibTeX )
B. Bérard, A. Labroue and Ph. SchnoebelenVerifying Performance Equivalence for Timed Basic Parallel ProcessesIn FoSSaCS 2000, LNCS 1784, pages 35-47. Springer, 2000. ( PS | PS.GZ | BibTeX )
F. Laroussinie and Ph. SchnoebelenThe State-Explosion Problem from Trace to Bisimulation EquivalenceIn FoSSaCS 2000, LNCS 1784, pages 192-207. Springer, 2000. ( 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 ICALP'99, LNCS 1644, pages 301-310. Springer, 1999. ( 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 ICALP'98, LNCS 1443, pages 103-115. Springer, 1998. ( PS | PS.GZ | BibTeX + Abstract )
A. Finkel and Ph. SchnoebelenFundamental Structures in Well-Structured Infinite Transition SystemsIn LATIN'98, LNCS 1380, pages 102-118. Springer, 1998. ( PS | PS.GZ | BibTeX )
1997
O. Kouchnarenko and Ph. SchnoebelenA Model for Recursive-Parallel ProgramsIn INFINITY'96, 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 PaCT'97, LNCS 1277, pages 45-59. Springer, 1997. ( PS | PS.GZ | BibTeX )
1996
O. Kouchnarenko and Ph. SchnoebelenModèles formels pour les programmes récursifs-parallèlesIn RENPAR'96, pages 85-88. 1996. ( 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 AMAST'93, 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 ICCI'94, pages 230-246. 1994. ( 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 STACS'94, LNCS 775, pages 47-58. Springer-Verlag, 1994. ( BibTeX )
1992
C. Autant and Ph. SchnoebelenPlace Bisimulations in Petri NetsIn APN'92, LNCS 616, pages 45-61. Springer-Verlag, 1992. ( 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 CONCUR'91, LNCS 527, pages 480-494. Springer-Verlag, 1991. ( BibTeX )
C. Autant, Z. Belmesk and Ph. SchnoebelenStrong Bisimilarity on Nets RevisitedIn PARLE'91, LNCS 506, pages 295-312. Springer-Verlag, 1991. ( 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 APN'90, pages 451-470. 1990. ( 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 ESOP'90, LNCS 432, pages 377-388. Springer-Verlag, 1990. ( BibTeX )
1989
Ph. Schnoebelen and Ph. JorrandPrinciples of FP2: Term Algebras for Specification of Parallel MachinesIn Languages for Parallel Architectures: Design, Semantics, Implementation Models, chapter 5, pages 223-273. John Wiley & Sons, Ltd., 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 ALP'88, LNCS 343, pages 233-243. Springer-Verlag, 1988. ( BibTeX )
1987
P. Schäfer and Ph. SchnoebelenSpecification of a Pipelined Event-Driven Simulator Using FP2In PARLE'87, LNCS 258, pages 311-328. Springer-Verlag, 1987. ( BibTeX )
Ph. SchnoebelenRewriting Techniques for the Temporal Analysis of Communicating ProcessesIn PARLE'87, LNCS 259, pages 402-419. Springer-Verlag, 1987. ( BibTeX )

About LSV

Search this list

Search the LSV database

highlight select