Download full bibliography (as BibTex): PaVeS publications

Our previous work in the field of parametrized synthesis and verification: previous work


2020

  • Esparza, J., Kret\'ınský, J., Sickert, S.: A Unified Translation of Linear Temporal Logic to ω-Automata. J. ACM. 67, (2020)
    LTL OmegaAutomata myown

    URL: Link
    Abstract BibTeX EndNote URL
  • Balasubramanian, A.R., Walukiewicz, I.: Characterizing Consensus in the Heard-Of Model. In: Konnov, I. and Kovács, L. (eds.) 31st International Conference on Concurrency Theory (CONCUR 2020). p. 9:1--9:18. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2020)
    HeardOfmodel consensusproblem myown verification

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Blondin, M., Esparza, J., Genest, B., Helfrich, M., Jaax, S.: Succinct Population Protocols for Presburger Arithmetic. In: Paul, C. and Bläser, M. (eds.) STACS. pp. 40:1-40:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
    myown populationprotocols succinct synthesis

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Seidl, H., Müller, C., Finkbeiner, B.: How to Win First-Order Safety Games. In: Beyer, D. and Zufferey, D. (eds.) VMCAI. pp. 426-448. Springer (2020)
    gametheory myown safety

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Irène Durand, B.C., Raskin, M.: On defining linear orders by automata. Moscow Journal of Combinatorics and Number Theory. 9, 253-291 (2020)
    automata expressivepower myown

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • D'Antoni, L., Helfrich, M., Kretinsky, J., Ramneantu, E., Weininger, M.: Automata Tutor v3. In: Lahiri, S.K. and Wang, C. (eds.) CAV (2). pp. 3-14. Springer (2020)
    tool

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Konnov, I., Lazic, M., Stoilkovska, I., Widder, J.: Tutorial: Parameterized Verification with Byzantine Model Checker. In: Gotsman, A. and Sokolova, A. (eds.) FORTE. pp. 189-207. Springer (2020)
    parametrizedverification verification

    URL: Link
    BibTeX EndNote URL
  • Jaax, S., Kiefer, S.: On Affine Reachability Problems. In: Esparza, J. and Král', D. (eds.) MFCS. p. 48:1--48:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
    affine-reachability scalar-reachability vector-reachability

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Inf. 57, 3-36 (2020)
    LTL myown sy synthesis

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Esparza, J., Helfrich, M., Jaax, S., Meyer, P.J.: Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs. CoRR. abs/2007.07638, (2020)
    myown parametrizedverification populationprotocols preprint tool

    Preprint: Link (to appear in ATVA20)
    Abstract BibTeX EndNote URL
  • Sickert, S., Esparza, J.: An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata. Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 831–844. Association for Computing Machinery, Saarbrücken, Germany (2020)
    AlternatingAutomata DeterministicForm LinearLogic Normal Temporal Weak

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Balasubramanian, A.R.: Complexity of controlled bad sequences over finite sets of Nd. In: Hermanns, H., Zhang, L., Kobayashi, N., and Miller, D. (eds.) LICS. pp. 130-140. ACM (2020)
    complexity myown

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Blondin, M., Esparza, J., Helfrich, M., Kucera, A., Meyer, P.J.: Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. In: Lahiri, S.K. and Wang, C. (eds.) CAV (2). pp. 372-397. Springer (2020)
    liveness parametrizedverification populationprotocols replicated systems verification

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Balasubramanian, A.R., Esparza, J., Lazic, M.: Complexity of Verification and Synthesis of Threshold Automata. CoRR. abs/2007.06248, (2020)
    complexity myown preprint synthesis thresholdautomata verification

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Courcelle, B., Durand, I., Raskin, M.: A unified algorithm for colouring graphs of bounded clique-width. (2020)
    finiteautomata graphexploration myown

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Raskin, M., Weil-Kennedy, C.: Efficient Restrictions of Immediate Observation Petri Nets. Presented at the (2020)
    immediateobservation myown reachability

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Raskin, M.: Constructive expressive power of population protocols, (2020)
    expressivepower myown populationprotocols

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Raskin, M., Weil-Kennedy, C., Esparza, J.: Flatness and Complexity of Immediate Observation Petri Nets. 31st International Conference on Concurrency Theory (CONCUR 2020). Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
    flatness immediateobservation myown reachability

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Esparza, J., Reiter, F.: A Classification of Weak Asynchronous Models of Distributed Computing. In: Konnov, I. and Kovács, L. (eds.) 31st International Conference on Concurrency Theory (CONCUR 2020). p. 10:1--10:16. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2020)
    asyncronous classification distributedalgorithms myown

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Bozga, M., Esparza, J., Iosif, R., Sifakis, J., Welzel, C.: Structural Invariants for the Verification of Systems with Parameterized Architectures. In: Biere, A. and Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I. p. 228--246. Springer (2020)
    invariants myown parameterizedverification verification

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Blondin, M., Raskin, M.A.: The Complexity of Reachability in Affine Vector Addition Systems with States. In: Hermanns, H., Zhang, L., Kobayashi, N., and Miller, D. (eds.) LICS. pp. 224-236. ACM (2020)
    VAS complexity myown rachability

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL

2019

  • Esparza, J.: Coffee and Cigarettes. In: Reisig, W. and Rozenberg, G. (eds.) Carl Adam Petri: Ideas, Personality, Impact. pp. 97-103. Springer (2019)
    petrinets

    URL: Link
    Abstract BibTeX EndNote URL
  • Jaax, S., Kiefer, S.: On Semigroups of Two-Dimensional Upper-Triangular Integer Matrices. CoRR. abs/1905.05114, (2019)
    groups matrix reachability semi

    Preprint: Link
    BibTeX EndNote URL
  • Esparza, J., Raskin, M., Weil-Kennedy, C.: Parameterized Analysis of Immediate Observation Petri Nets. In: Donatelli, S. and Haar, S. (eds.) Petri Nets. pp. 365-385. Springer (2019)
    immediateobservation populationprotocols

    URL: Link
    Abstract BibTeX EndNote URL
  • Blondin, M., Esparza, J., Jaax, S.: Expressive Power of Oblivious Consensus Protocols, http://arxiv.org/abs/1902.01668, (2019)
    broadcast population protocols

    URL: Link
    Abstract BibTeX EndNote URL
  • Meyer, P.J., Esparza, J., Offtermatt, P.: Computing the Expected Execution Time of Probabilistic Workflow Nets. In: Vojnar, T. and Zhang, L. (eds.) TACAS (2). pp. 154-171. Springer (2019)
    expectedterminationtime petrinets

    URL: Link
    Abstract BibTeX EndNote URL
  • Raskin, M., Welzel, C.: Working with first-order proofs and provers. European Lisp Symposium (2019)
    automatedtheoremprovers firstorderlogic interactiveproofsystems

    URL: Link
    BibTeX EndNote URL
  • Raskin, M.: Population protocols with unreliable communication. CoRR. abs/1902.10041, (2019)
    broadcastprotocols faulttolerance populationprotocols

    Preprint: Link
    BibTeX EndNote URL
  • Goubault, É., Lazic, M., Ledent, J., Rajsbaum, S.: Wait-Free Solvability of Equality Negation Tasks. In: Suomela, J. (ed.) DISC. pp. 21:1-21:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
    myown

    URL: Link
    Abstract BibTeX EndNote URL
  • Blondin, M., Esparza, J., Jaax, S.: Expressive Power of Broadcast Consensus Protocols. In: Fokkink, W. and van Glabbeek, R. (eds.) 30th International Conference on Concurrency Theory (CONCUR 2019). p. 31:1--31:16. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019)
    broadcast complexity protocols

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Berkovits, I., Lazic, M., Losa, G., Padon, O., Shoham, S.: Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics. In: Dillig, I. and Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II. p. 245--266. Springer (2019)
    distributedalgorithms myown parameterizedverification

    URL: Link
    Abstract BibTeX EndNote URL
  • Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. In: Fokkink, W. and van Glabbeek, R. (eds.) CONCUR. pp. 33:1-33:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
    distributedalgorithms myown parametrizedverification randomizedconsensus

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Raskin, M., Simkin, M.: Perfectly Secure Oblivious RAM with Sublinear Bandwidth Overhead. In: Galbraith, S.D. and Moriai, S. (eds.) Lecture Notes in Computer Science. p. 537--563. Springer International Publishing (2019)
    cryptography myown protocols security

    URL: Link
    BibTeX EndNote URL
  • Hansen, K.A., Raskin, M.: A Stay-in-a-Set Game without a Stationary Equilibrium. Electronic Proceedings in Theoretical Computer Science. 305, 83--90 (2019)
    gametheory myown safetyconditions verification

    URL: Link
    BibTeX EndNote URL
  • Esparza, J., Jaax, S., Raskin, M.A., Weil-Kennedy, C.: The Complexity of Verifying Population Protocols. CoRR. abs/1912.06578, (2019)
    complexity myown parametrizedverification populationprotocols verification

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Goubault, É., Lazic, M., Ledent, J., Rajsbaum, S.: A Dynamic Epistemic Logic Analysis of the Equality Negation Task. In: Barbosa, L.S. and Baltag, A. (eds.) DaLí. pp. 53-70. Springer (2019)
    logic myown

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Blondin, M., Haase, C., Mazowiecki, F., Raskin, M.: Affine Extensions of Integer Vector Addition Systems with States. (2019)
    complexity myown reachability

    Preprint: Link (25 pages, 7 figures)
    Abstract BibTeX EndNote URL

2018

  • Blondin, M., Esparza, J., Kucera, A.: Automatic Analysis of Expected Termination Time for Population Protocols. In: Schewe, S. and Zhang, L. (eds.) 29th International Conference on Concurrency Theory (CONCUR 2018). pp. 33:1-33:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)
    ExpectedTerminationTime PerformanceAnalysis PopulationProtocols

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL
  • Esparza, J., Ganty, P., Majumdar, R., Weil-Kennedy, C.: Verification of Immediate Observation Population Protocols. In: Schewe, S. and Zhang, L. (eds.) 29th International Conference on Concurrency Theory (CONCUR 2018). pp. 31:1-31:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)
    ImmediateObservation ParametrizedVerification PopulationProtocols

    URL: Link

    Preprint: Link
    Abstract BibTeX EndNote URL