Formal Methods and Verification at ULB   Computer Science Department at ULB  

Jean-Francois Raskin

Ph.D., F.U.N.D.P. (Belgium), 1999.

Professor

Département d'Informatique
Université Libre de Bruxelles
Bld du Triomphe CP 212
1050 Brussels, Belgium

Building: N.O., Office: N8.112
Phone: +32 2 650.55.92, Fax: +32 2 650.56.09
Email: jraskin@ulb.ac.be

>>> The Formal Methods and Verification Group at ULB <<<
>>>Centre Fédéré en Vérification <<<

>>>Computer Science Seminars <<<

Recent Past Events :


TIME 2005, June 23-25, Burlington, USA. PC member.
FORMATS 2005, Uppsalla, Sweeden, Sep. 2005. PC member.
Artist Summer School on Testing and Verification, Uppsala, Sweeden, Sep. 2005. Invited speaker.
BNAIC'05, Académie des Sciences de Bruxelles, 17-18 octobre 2005. PC member.
Movep06 - Bordeaux, France, June 2006. Invited Speaker
CONCUR06, Bonn, August 2006. PC Member
ACSD06, Turku, Finland, June 2006. PC Member
Infinity06, Bonn, August 2006. PC Member
FORMATS06, Paris, France, September. PC Member
Journée de l'Informatique Fondamentale du FNRS , 18/10/2006, Organizer.
Workshop "Ten years after the barrier verification", Twente, Nov. 2006, Twente, Invited speaker.
MOTIVES, Feb. 19-23, 2006, Trento, Italy, Invited speaker.
HSCC'07, Pisa, Italy, April 3-5, 2007 , PC Member.
VMCAI'07, Nice, France, January 14-16, 2007 , PC Member.
ACSD'07, PC Member.
FORMATS'07, co-Chairman.
AFADL'07, PC Member.
ACSD'08, PC Member.
TIME'08, PC Member.
FOSSACS'08, PC Member.
QAPL'08, Invited Speaker.
FORMATS'08, PC Member.
ARTIST 2 School, Shanghai, Invited Speaker.
Automata and Verification, Mons, August 08.
FOSSACS'09, PC Member.
ACSD'09, PC Member.
APNOC'09, PC Member.
TiSto'09, PC Member.
CSL'09, PC Member.
TIME'09, co-Chairman.
AutomathA'09, Invited Speaker.
ESF Games Summer School'09.
GASICS workshop at CAV09, co-organizier

Upcoming Events :

ACSD 2010, PC Member.
HSCC 2010, PC Member.
CAV 2010, PC Member.
TACAS 2010, Invited Speaker.
AVACS School, Invited Speaker.
Logic for Systems Analysis, PC Member.
TIME 2010, PC Member.
MOVEP 2010, PC Member.
ARTIST Design School, Invited Speaker.
Logics in security workshop 2010, PC Member.
Games, Automata, Logic, and Formal Languages (GandALF) 2010, PC Member.
VECoS'2010, PC Member.
GASICS Workshop at CONCUR2010, Co-organizer.

ShortCV -- Projects -- Collaborations-- Publications -- Teaching

 
Short Curriculum Vitae

Jean-François Raskin was born in Belgium, in 1972. He received his master and Ph.D. degrees in computer science from the Université de Namur, Belgium, in june 1995 and april 1999, respectively. From 1995 to 1999, he was a Research Associate (aspirant) of the Belgian National Fund for Scientific Research (FNRS), Université de Namur, Belgium.  He worked on the decidability,complexity and expressiveness of formalisms for reasoning about real-time systems.

After long research stays at the University of California at Berkeley, Max-Planck Institute for Computer Science (Saarbrucken), and ENS Paris, he is a Professor at the computer science department  of the Université Libre de Bruxelles (ULB), Belgium. His research interests are the formal methods for the verification of concurrent, real-time, and hybrid systems. More precisely, his research focusses on:

    • Logic formalisms, especially temporal logics and real-time logics;
    • Automata formalisms and their extensions for real-time and hybrid systems;
    • Abstract interpretation theory and its application to the verification of concurrent, real-time and hybrid systems ;
    • Game theory for synthesis of controllers.
For more details about his research, see the page of the group for Formal Methods and Verificiation at ULB.

At the ULB, he teaches subjects in theoretical computer science : automatic proofs and proofs of programs, logic in computer science, computability and complexity, and analysis of hybrid systems. He is also the secretary of the Belgian F.N.R.S. contact group on Theoretical Computer Science.

>> You can also download here a more complete CV.<<
 

Projects

Centre Fédéré en Vérification

PAI-Moves

Quasimodo

Gasics

Team

Current PhD Students

Marc Ducobu

Nicolas Maquet

Frédéric Servais

Current Post-Docs

Naiyong Jin

Tristan Legal

Nathalie Snjazder

Aldric Degorre

Emmaunuel Filiot

Visitors

Barbara di Giampaolo

Wouter Kuiper

Former PhD Students

Steve Kremer, Formal Analysis of Optimistic Fair Exchange Protocols. December 2003. (Now INRIA researcher at LSV-Cachan)

Laurent Van Begin, Efficient Verification of Counting Abstractions for Parametric Systems. December 2003. 

Laurent Doyen. Algorithmic Analysis of Complex Semantics for Timed and Hybrid Systems. June 2006. (Now CNRS researcher at LSV-Cachan).

Martin De Wulf. From Timed Models to Timed Implementations. December 2006.

Pierre Ganty. The Fixpoint Checking Problem: an Abstraction Refinement Perspective. September 2007. (Now assistant Professor at IMDEA, Madrid).

Gilles Geeraerts. Coverability and Expressiveness Properties of Well Structured Transition Systems. March 2007. (Now Assistant Professor at ULB).

Former Post-Docs

Nicolas Markey (Now CNRS researcher at LSV-ENS Cachan).

Sébastien Bardin (Now at CEA Saclay, France).

Pierre-Alain Reynier (Now Assistant Professor at Université de Marseille).

Raffaella Gentilini (Now Assitant Professor at University of Perugia).
 

Collaborations

Our research group has collaborations with the following groups:


Main publications
My DBLP page
Google Scholar me

PDF of my (recent) papers can be downloaded here

Please email me if you do not find the one you want !



    2010

  • Lubos Brim, Jakub Chaloupka, Laurent Doyen, Rafaella Gentilini, and Jean-François Raskin. Faster Algorithms for Mean-Payoff Games. 19 pages. January, 2010. Submitted.
  • Pierre Ganty, Nicolas Maquet, and Jean-François Raskin. Fixpoint Guided Abstraction for Alternating Automata. Extended invited version. Submitted. 20 pages.
  • Andreas Classen, Patrick Heymans, Axel Legay, Jean-François Raskin, and Pierre-Yves Schobbens. Model Checking lots of Systems: Efficient Verification of Temporal Properties in Software Product Lines. To appear in International Conference Software Engineering 2010, IEEE, Cape Town, 10 pages. 2010.
  • Emmanuel Filiot, Tristan Le Gall, Jean-François Raskin. Regret Minimization in Game Graphs. 15 pages. Submitted for publication. 2010.  
  • G. Geeraerts, G. Kalyon, T. Le Gall, N. Maquet, and J.-F. Raskin. Lattice-Valued Binary Decision Diagrams. 25 pages. Submitted for publication. 2010.
  • Emmanuel Filiot, Nayiong Jin, and Jean-François Raskin. Compositional Algorithms for LTL Synthesis. 18 pages. Submitted for publication. 2010.
  • Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin, and Szymon Torunczyk. Energy and Mean-Payoff Games with Imperfect Information. 12 pages. Submitted for publication. 2010.
  • Laurent Doyen and Jean-François Raskin. Antichain Algorithms for Finite Automata. To appear in TACAS2010, LNCS, Springer 20 pages. 2010.
  • Laurent Doyen and Jean-François Raskin. Games with Imperfect Information: Theory and Algorithms. Lecture notes for the summer school "Games". 25 pages. To appear in Cambridge University Press. 2010.
          2009 
  • Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. On the efficient computation of the coverability set for Petri nets. To appear in the International Journal of Foundations of Computer Science.31 pages.
  • Pierre Ganty, Gilles Geeraerts, Jean-François Raskin, Laurent Van Begin. Méthodes algorithmiques pour l'analyse des réseaux de Petri.  To appear in Techniques et sciences informatiques. 2008.
  • Jean-François Raskin. Exploiting Structure in Automata Constructions (abstract). Invited talk at the General Meeting of the Authomatha project. 3 pages. Liège, 2009.
  • Laurent Doyen, Gilles Geeraerts, Jean-François Raskin, and Julien Reichert. Realizability of Real-time Logics. In FORMATS09, LNCS 5813, Springer, pp.133-148 2009.
  • Pierre Ganty, Nicolas Maquet, and Jean-François Raskin. Fixpoint Guided Abstraction for Alternating Automata. In CIAA'09, LNCS 5642, Springer, pp.155-164, 2009.
  • Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. An Antichain Algorithm for LTL Realizability. In CAV'09, LNCS 5643, Springer, pp.263-277, 2009.
  • Laurent Doyen and Jean-François Raskin. Improved Algorithms for the Automata-Based Approach to Model-Checking. In Journal of Logical Methods in Computer Science-5(1:5)2009.
  • Franck Cassez, Jan J. Jessen, Kim Larsen, Jean-François Raskin, and Pierre-Alain Reynier. Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study. In HSCC'09, LNCS 5469, Springer, pp. 90-104, 2009.

    • 2008

  • Martin De Wulf, Laurent Doyen, Nicolas Maquet, and Jean-François Raskin. Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking. In TACAS'08, LNCS 4963, Springer, pp. 63-77, 2008.
  • Laurent Doyen, Tom Henzinger, and Jean-François Raskin. Equivalence of Labelled Markov Chains. In International Journal of Foundations of Computer Science, 19(3):549-563, 2008.
  • Pierre Ganty, Jean-François Raskin, Laurent Van Begin. From Many Places to Few: Automatic Abstraction Refinement for Petri Nets. Invited extended version. In Fundamenta Informaticae:88(3), 275-305, 2008.
  • Jean-François Raskin and Frédéric Servais. Visibly Pushdown Transducers. In ICALP'08, LNCS 5126, Springer, pp. 386-397, 2008.
  • Martin De Wulf, Laurent Doyen, Nicolas Marquet, and Jean-François Raskin. LTL Satisfiability, Alternating Büchi Automata Emptiness, and Model-Checking with ALASKA. In ATVA'08, LNCS 5311, Springer, pp. 240-245, 2008.
  • Martin De Wulf, Laurent Doyen, Nicolas Markey, Jean-François Raskin: Robust safety of timed automata. Formal Methods in System Design 33(1-3): 45-84 (2008)
  • Véronique Bruyère, Emmanuel Dal'ollio, and Jean-François Raskin. Durations and Parametric Model-Checking in Timed Automata. In Transactions on Computational Logic, 9(2), 21 pages, ACM press, 2008.

    2007

  • Jean-Francois Raskin. Controller Synthesis using Lattice Theory. Invited tutorial. Proceeding of the 46th conference on Decision and Control (CDC 2007), IEEE press. New-Orleans. December 2007. (4 pages)
  • Gilles Geeraerts, Jean-Francois Raskin, and Laurent Van Begin. Well-structured Languages. In Acta Informatica 44(3-4):249-288, Springer, 2007.
  • Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. On the efficient computation of the coverability set for Petri nets. In ATVA'07, LNCS 4762, Springer, pp.98-113, 2007.
  • Franck Cassez, Alexandre David, Didier Lime, Kim Larsen, and Jean-François Raskin. Timed Control with Observation Based and Stuttering Invariant Strategies. In ATVA'07, LNCS 4762, Springer, pp.192-206, 2007.
  • Patrick Cousot, Pierre Ganty, and Jean-Francois Raskin. Fixpoint-based Abstraction Refinement. In SAS'07, LNCS 4634, Springer, pp.333-348, 2007.
  • Thomas Brihaye, Thomas A. Henzinger, Vinayak S. Prabhu, and Jean-Francois Raskin. Minimum-Time Reachability in Timed Games. In ICALP'07, LNCS 4596, Springer, pp.825-837, 2007.
  • Khrishnendu Charterjee, Laurent Doyen, Thomas A. Henzinger and Jean-Francois Raskin. Algorithms for Omega-regular games of Incomplete Information (extended version). Accepted for publication in Logical Methods in Computer Science, 2007. (30 pages).
  • Thomas Brihaie, Patricia Boyer, Véronique Bruyère, Jean-François Raskin. On the Optimal Reachability Problem for Timed Automata. In Formal Methods in Systems Design 31(2):135-175, Springer, 2007.
  • Pierre Ganty, Jean-François Raskin, Laurent Van Begin. From Many Places to Few: Automatic Abstraction Refinement for Petri Nets. In ICATPN'07, LNCS 4546, Springer, pp.124-143, 2007.
  • Véronique Bruyère and Jean-François Raskin. Real-Time Model-Checking: Parameters Everywhere (extended version). In Logical Methods in Computer Science 3(1):1-30, 2007.
  • Laurent Doyen and Jean-François Raskin. Improved Algorithms for the Automata-based Approach to Model-Checking. In TACAS'07, LNCS 4424,  Springer Verlag, 2007.
  • Véronique Bruyère and Jean-Francois Raskin. Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic. In Transactions in Computatitonal Logic 9(2), ACM Press, 2007.

2006

  • Khrishnendu Charterjee, Laurent Doyen, Thomas A. Henzinger and Jean-Francois Raskin. Algorithms for Omega-regular games of Incomplete Information. In CSL'06, Lecture Notes in Computer Science, 4207, 287-302, 2006. (16 pages)
  • Jean-Francois Raskin and Frédéric Servais. On the Symbolic Computation of the Hardest Configurations of the Rush Hour Game. To appear in CG'06, Lecture Notes in Computer Science. (12 pages)
  • Martin De Wulf, Laurent Doyen, Thomas A. Henzinger and Jean-Francois Raskin. Antichains: a New Algorithm to Solve Universality of FA. In CAV'06, Lecture Notes in Computer Science, 4144, Springer-Verlag, pp. 17-30, 2006.
  • Martin De Wulf, Laurent Doyen, and Jean-Francois Raskin. A Lattice Theory for Solving Games of Imperfect Information. In HSCC'06, Lecture Notes in Computer Science, 3927, pp. 153-168, Springer-Verlag, 2006.
  • Pierre Ganty, Jean-François Raskin, and Laurent Van Begin. A Complete Abstract Interpretation Framework for Coverability Properties of WSTS. In VMCAI'06, Lecture Notes in Computer Science 3855, pp. 49-64, Springer Verlag, 2006.
  • Nicolas Markey and Jean-François Raskin. Model-Checking Restricted Sets of Timed Paths (extended version). In Theoretical Computer Science, 358(2-3):273--292, Elsevier Science, 2006.
  • Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On Model-Checking Timed Automata with Stopwatch Observers. In Information and Computation, 204:408--433, Elservier Sciences, 2006.
  • Alain Finkel, Gilles Geeraerts, Jean-François Raskin and Laurent Van Begin. On the Omega-Language Expressive Power of Extended Petri Nets (extended version). In Theoretical Computer Science, 356(3):374--386, Elsevier Sciences, 2006.

    2005

  • Laurent Doyen, Tom Henzinger, Jean-François Raskin. Automatic Rectangular Refinement of Affine Hybrid Systems. In FORMATS'05, Lecture Notes in Computer Science 3829, pp. 144--161,Springer-Verlag, 2005.
  • Gilles Geeraerts, Jean-Francois Raskin and Laurent Van Begin. Expand,Enlarge, and Check. New Algorithms to Solve the Coverability Problem of WSTS (extended version). In Journal of Computer and System Sciences, 72(1):180-203, Elsevier Sciences, 2005. 
  • Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On Optimal Timed Strategies. In FORMATS'05, Lecture Notes in Computer Science 3829, pp. 49--64, Springer-Verlag, 2005.
  • Martin De Wulf, Laurent Doyen, Jean-François Raskin. Systematic Implementations of Timed Models. In FM'05, Lecture Notes in Computer Science 3582, pp. 139--156, Springer-Verlag, 2005.
  • Martin De Wulf, Laurent Doyen, Jean-François Raskin. Almost ASAP Semantics: from Timed Models to Timed Implementations (extended version).In Formal Aspect of Computing, 17(3):319--341, Springer-Verlag, 2005.
  • Jean-François Raskin. An Introduction to Hybrid Automata. In Handbook of Networked and Embedded Control Systems, pp 491-518, Dimitrios Hristu-Varsakelis, William S. Levine (Eds.), Birkhauser, 2005, ISBN 0-8176-3239-5.
  • Gilles Geeraerts, Jean-Francois Raskin, and Laurent Van Begin. Expand, Enlarge and Check Made Efficient. In CAV'05, Lecture Notes in Computer Science 3576, pp. 394--407, Springer-Verlag, 2005.
  • Alain Finkel, Gilles Geeraerts, Jean-Francois Raskin, and Laurent Van Begin. On the omega-language expressive power of extended Petri nets. In Electronic Notes in Theoretical Computer Science, Volume 128, Issue 2, pp 87-101, 2005. 
  • Thomas Henzinger, Rupak Manjumdar, and Jean-François Raskin. A Classification of Symbolic Transition Systems. In Transactions on Computational Logic, Volume 6, Number 1, pp 1-31, ACM Press, 2005.
  • Jean-Francois Raskin and Laurent Van Begin. Games for Counting Abstractions. In Electronic Notes in Theoretical Computer Science, 128(6):69-85, Elsevier Science, 2005.

    2004

  • Giorgio Delzanno, Jean-Francois Raskin, and Laurent Van Begin. Covering Sharing-Trees: a Compact Data-Structure for Parametrized Verification. In the Journal of Software Tools for Technology Transfer, Volume 5, Numbers 2-3, pp 268-297, Springer Verlag, March 2004. [Postscript]
  • Martin De Wulf, Laurent Doyen, Nicolas Markey, and Jean-François Raskin. Robustness and Implementability of Timed Automata. In FORMATS'04, Lecture Notes in Computer Science, 3253, pp. 118-133, Springer Verlag, 2004.
  • Gilles Geeraerts, Jean-Francois Raskin, and Laurent Van Begin. Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS. In FSTTCS'04, Lecture Notes in Computer Science, 3328, pages 287--298. Springer-Verlag, 2004.
  • Jean-françois Raskin and Laurent Van Begin. Petri with Non-blocking Arcs are Difficult to Analyze. In Electronic Notes in Theoretical Computer Science, 98, 35-55, Elsevier Science, 2004 [Postscript]
  • Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin.  Model-Checking Weigthed Timed Automata. In FORMATS'04, Lecture Notes in Computer Science, 3253, pp. 277-292, Springer Verlag, 2004.
  • Nicolas Markey and Jean-François Raskin. Model-Checking Restricted Sets of Timed Paths. In CONCUR'04, Lecture Notes in Computer Science, 3170, pp. 432-447, Springer-Verlag, 2004.
  • Martin De Wulf, Laurent Doyen, Jean-François Raskin. Almost ASAP Semantics: From Timed Models to Timed Implementations. In HSCC'04, Lecture Notes in Computer Science, 2993, pp 296-310, 2004. [Postscript]

    2003

  • Jean-françois Raskin, Mathias Samuelides, and Laurent Van Begin. Petri Games are Monotonic but Difficult to Decide. Technical Report 508, ULB, 2003. [Postscript]
  • Steve Kremer and Jean-François Raskin. A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols (Extended Version). In Journal of Computer Security, 11(3), 399-430, Ios Press. 2003.  [Postscript]
  • Véronique Bruyère, Jean-François Raskin. Real-time Model-checking: Parameters Everywhere ! In the In FSTTCS'03, Lecture Notes in Computer Science, 2914, pp. 100-111, Springer-Verlag, 2003. [Postscript]
  • Véronique Bruyère, Emmanuel Dall'Olio, Jean-François Raskin. Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic. In STACS'03, Lecture Notes in Computer Science, 2607, Berlin, 2003. [Postscript]

    2002

  • Alain Finkel, Jean-François Raskin, Mathias Samuelidis, and Laurent Van Begin. Monotonic Extensions of Petri Nets: Forward and Backward Search Revisited. In the proceedings of INFINITY'02, Electronic Notes in Theoretical Computer Science, Volume 68, Issue 6, Elsevier, Brno, 2002. (20 pages) 
  • Jean-Francois Raskin, Pierre-Yves Schobbens, Thomas A. Henzinger and Laurent F'erier. Axioms for Real-Time Logics. In Theoretical Computer Science, 274(1-2), 151-182, Elsevier Science, 2002.
  • Thierry Massart, Jean-françois Raskin, and Laurent Van Begin. Symbolic Distributed Verification of a Class of Parametric Concurrent Systems. In the proceedings of PDMC'02, Brno, 2002. (6 pages) [Postscript]
  • Giorgio Delzanno, Jean-François Raskin and Laurent Van Begin. Towards Automated Verification of Multithreaded Java Programs. In the Proc. of TACAS'02, Lecture Notes in Computer Science, 2280, Springer, pp 173-187. 2002. [Postscript]
  • Franck Cassez, Thomas Henzinger, and Jean-François Raskin. A Comparison of Control Problems for Timed and Hybrid Systems. In HSCC'02, Lecture Notes in Computer Science, 2289, pp. 134-148, Springer-Verlag, 2002 (18 pages) [Postscript]
  • Steve Kremer and Jean-François Raskin. Game Analysis of Abuse-free Contract Signing . In Computer Security Foundations Workshop 2002 (CSFW 2002),Cape Breton, Nova Scotia, Canada (15 pages).  [Postscript]

    2001

  • Steve Kremer and Jean-François Raskin. A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols . In CONCUR 2001-Concurrency Theory,, Aalborg, Danemark, August 2001 (15 pages).  [Postscript]
  • Giorgio Delzanno, Jean-François Raskin and Laurent Van Begin. Attacking Symbolic State Explosion in Parametrized Verification. In the Proc. of CAV'01: International Conference on Computer Aided Verification, Lecture Notes in Computer Science, 2102, Springer, pp 298-310, Paris, 2001. [Postscript]

    2000

  • Thomas Henzinger and Jean-François Raskin. Robust Undecidability of Timed and Hybrid Systems. In HSCC'00, Lecture Notes in Computer Science, 1790, pp. 145-159, Springer Verlag, 2000. [Postscript]
  • Giorgio Delzanno and Jean-Francois Raskin. Symbolic Representation Of Up-Ward Closed Sets. In Tacas'00, Lecture Notes In Computer Science 1785, Pp. 426-440, Springer-Verlag, 2000.
  • Thomas A. Henzinger, Freddy Mang, Rupak Manjumdar and Jean-Francois Raskin. Abstract Interpretation of Game Properties. In SAS'00, Lecture Notes in Computer Science 1824, pp. 220-239, Springer-Verlag, 2000.
  • Jean-François Raskin and Pierre-Yves Schobbens. Automata for Qualitative Real-Time. In the proceedings of Les journées montoises de l'informatique théorique, Marnes-La-Vallée, France, March 2000. [Postscript]
  • Steve Kremer and Jean-François Raskin. Formal Verification of Non-Repudiation Protocols- A Game Approach . In Formal Methods for Computer Security, Chicago, USA, July 2000 (13 pages).  [Postscript]
  • Steve Kremer and Jean-François Raskin. A Game Approach to the Verification of Exchange Protocols - Application to Non-Repudiation Protocols. In Workshop on Issues in the Theory of Security (WITS '00), Geneve, Switzerland, June 2000. (6 pages). [Postscript]

    1999

  • Jean-François Raskin and Pierre-Yves Schobbens. The Logic of Event Clocks, Decidability, Complexity,and Expressiveness. In Journal of Automata, Languages and Combinatorics, 4, 3, Otto-von-Guericke-Universität Magdeburg, September 1999. (37 pages) [Postscript]
  • Laurent Ferrier, Jean-François Raskin, and Pierre-Yves Schobbens. Models Generation of a Fictitious Clock Real-Time Logic Using Sharing-Trees. In Symbolic Model Checking 99, appeared as Volume 23, Issue 2 of Electronic Notes in Theoretical Computer Science, Trento, Italy, July 1999. [Postscript]
  • Jean-François Raskin. Logics, Automata and Classical Theories for Deciding Real Time. Ph. D. Thesis of the Computer Science Department. University of Namur, Belgium, April 1999. (223 pages) [Postscript]
  • Jean-François Raskin and Pierre-Yves Schobbens. The Logic of Initially and Next, Complete Axiomatisationand Complexity Issues. In Information ProcessingLetters, 69, Issue 5, pp 221-225, Elsevier Science, March 1999. [Postscript]

    1998

  • Thomas Henzinger, Jean-François Raskin, and Pierre-Yves Schobbens. Axioms for Real-Time Logics. In International Conference on Concurrency, Lecture Notes in Computer Science, 1466, Springer-Verlag, Nice, France, August 1998. [Postscript]
  • Thomas Henzinger, Jean-François Raskin and Pierre-Yves Schobbens. The Regular Real-Time Languages. In International Colloquium on Automata, Languages,and Programming, Lecture Notes in Computer Science, 1443, Springer-Verlag, pp 580-591, Aalborg, Denmark, July 1998. [Postscript]

    1997

  • Jean-François Raskin and Pierre-Yves Schobbens. Real-Time Logics : Fictitious Clock as an Abstraction of Dense Time. In Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science,  1217, Springer Verlag, pp165-182, Twente,The Netherlands, April 1997. [Postscript]
  • Jean-François Raskin and Pierre-Yves Schobbens. State Clock Logic: a Decidable Real-Time Logic .In  Hybrid and Real-Time Systems, Lecture Notes in Computer Science, 1201, Springer Verlag, pp 31-47, Grenoble, France, March 1997. [Postscript]
Teaching (in french)

INFO-F-408 et INFO-F-421. Calculabilité et complexité - Supplément de Calculabilité et complexité.Slides. Slides 2
INFO-F-513. Vérification 2. Description du cours.
INFO-F-302. Logique pour l'informatique.
INFO-F-502. Séminaire d'informatique approfondie.

Last updated: september 2008.