Ocan
Sankur
Research
Teaching
Contact
@article{andre2024parameterized, title={Parameterized Verification of Timed Networks with Clock Invariants}, author={Andr{\'e}, {\'E}tienne and Jacobs, Swen and Karra, Shyam Lal and Sankur, Ocan}, journal={arXiv preprint arXiv:2408.05190}, pdf={https://arxiv.org/pdf/2408.05190}, year={2024} } @inproceedings{desbois:hal-04650916, TITLE = {{An Efficient Modular Algorithm for Connected Multi-Agent Path Finding}}, AUTHOR = {Victorien Desbois and Ocan Sankur and François Schwarzentruber}, URL = {https://hal.science/hal-04650916}, BOOKTITLE = {{27th European Conference on Artificial Intelligence}}, ADDRESS = {Santiago de Compostela, Spain}, YEAR = {2024}, MONTH = Oct, PDF = {https://hal.science/hal-04650916/file/main.pdf}, HAL_ID = {hal-04650916}, HAL_VERSION = {v1}, } @unpublished{sankur:hal-04662214, TITLE = {{Online Test Synthesis From Requirements: Enhancing Reinforcement Learning with Game Theory}}, AUTHOR = {Ocan Sankur and Thierry Jéron and Nicolas Markey and David Mentré and Reiya Noguchi}, URL = {https://www.arxiv.org/abs/2407.18994}, NOTE = {working paper or preprint}, YEAR = {2024}, MONTH = Jul, booktitle={Preprint}, PDF = {https://hal.science/hal-04662214/file/paper.pdf}, HAL_ID = {hal-04662214}, HAL_VERSION = {v1}, } @unpublished{Sankur2024, author = {Ocan Sankur}, title = {Automatic Assume-Guarantee Reasoning for Safety and Liveness Using Passive Learning}, year = 2024, month = feb, booktitle={Preprint}, doi = {https://doi.org/10.21203/rs.3.rs-3910982/v1}, url = {https://doi.org/10.21203/rs.3.rs-3910982/v1}, pdf = {https://doi.org/10.21203/rs.3.rs-3910982/v1} } @article{DBLP:journals/corr/abs-2305-10546, author = {Nathana{\"{e}}l Fijalkow and Nathalie Bertrand and Patricia Bouyer{-}Decitre and Romain Brenguier and Arnaud Carayol and John Fearnley and Hugo Gimbert and Florian Horn and Rasmus Ibsen{-}Jensen and Nicolas Markey and Benjamin Monmege and Petr Novotn{\'{y}} and Mickael Randour and Ocan Sankur and Sylvain Schmitz and Olivier Serre and Mateusz Skomra}, title = {Games on Graphs}, journal = {CoRR}, volume = {abs/2305.10546}, year = {2023}, url = {https://doi.org/10.48550/arXiv.2305.10546}, doi = {10.48550/ARXIV.2305.10546}, eprinttype = {arXiv}, eprint = {2305.10546}, timestamp = {Thu, 25 May 2023 15:41:47 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2305-10546.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{CSS-aamas23, author = {Isseïnie Calviac and Ocan Sankur and François Schwarzentruber}, title = {Improved Complexity Results and an Efficient Solution for Connected Multi-Agent Path Finding}, editor = {}, booktitle = {22nd International Conference on Autonomous Agents and Multiagent Systems ({AAMAS}'23)}, acronym = {{AAMAS}'23}, publisher = {}, year = {2023}, month = may, doi = {}, note = {To~appear}, PDF={https://hal.science/hal-04075393} } @inproceedings{TS-tacas23, TITLE = {{PyLTA: A Verification Tool for Parameterized Distributed Algorithms}}, AUTHOR = {Bastien Thomas and Ocan Sankur}, URL = {}, BOOKTITLE = {{TACAS 2023 - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}}, ADDRESS = {Paris, France}, YEAR = {2023}, MONTH = Apr, PDF = {https://hal.science/hal-03996060v1}, } @inproceedings{sankur:hal-03947462, TITLE = {{Timed Automata Verification and Synthesis via Finite Automata Learning}}, AUTHOR = {Ocan Sankur}, URL = {https://hal.science/hal-03947462}, BOOKTITLE = {{TACAS 2023 - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}}, ADDRESS = {Paris, France}, YEAR = {2023}, MONTH = Apr, PDF = {https://hal.science/hal-03947462/file/main.pdf}, HAL_ID = {hal-03947462}, HAL_VERSION = {v1}, } @article{QUEFFELEC2022, title = {Complexity of Planning for Connected Agents in a Partially Known Environment}, journal = {Theoretical Computer Science}, year = {2022}, issn = {0304-3975}, doi = {https://doi.org/10.1016/j.tcs.2022.11.015}, url = {https://www.sciencedirect.com/science/article/pii/S030439752200679X}, author = {Arthur Queffelec and Ocan Sankur and François Schwarzentruber}, keywords = {multi-agent path finding, multi-agent planning, connectivity, imperfect knowledge, decentralized planning}, abstract = {The Connected Multi-Agent Path Finding (CMAPF) problem asks for a plan to move a group of agents in a graph while respecting a connectivity constraint. We study a generalization of CMAPF in which the graph is not entirely known in advance, but is discovered by the agents during their mission. We present a framework introducing this notion and study the problem of searching for a strategy to reach a configuration in this setting. We prove the problem to be PSPACE-complete when requiring all agents to be connected at all times, and NEXPTIME-hard in the decentralized case.}, PDF={https://hal.science/hal-03930625/file/main.pdf} } @inproceedings{fsttcs2022-BMSS, author ={Bertrand, Nathalie and Markey, Nicolas and Sadhukhan, Suman and Sankur, Ocan}, title ={{Semilinear Representations for Series-Parallel Atomic Congestion Games}}, booktitle ={42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)}, pages ={32:1--32:20}, series ={Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN ={978-3-95977-261-7}, ISSN ={1868-8969}, year ={2022}, volume ={250}, editor ={Dawar, Anuj and Guruswami, Venkatesan}, publisher ={Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address ={Dagstuhl, Germany}, URL ={https://drops.dagstuhl.de/opus/volltexte/2022/17424}, URN ={urn:nbn:de:0030-drops-174243}, PDF={https://hal.science/hal-03937259v1}, doi ={10.4230/LIPIcs.FSTTCS.2022.32}, annote ={Keywords: congestion games, Nash equilibria, Presburger arithmetic, semilinear sets, price of anarchy} } @inproceedings{atva2022-NSJMM, author = {Noguchi, Reiya and Sankur, Ocan and J{\'e}ron, Thierry and Markey, Nicolas and Mentr{\'e}, David}, title = {Repairing Real-Time Requirements}, editor = {Bouajjani, Ahmed and Hol{\'\i}k, Luk{\'a}{\v s} and Wu, Zhilin}, booktitle = {{P}roceedings of the 20th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'22)}, acronym = {{ATVA}'22}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, year = {2022}, month = oct, doi = {10.1007/978-3-031-15839-1_11}, note = {To~appear}, PDF = {https://hal.science/hal-03777464} } @inproceedings{DBLP:conf/formats/BouyerGHSS22, author = {Patricia Bouyer and Paul Gastin and Fr{\'{e}}d{\'{e}}ric Herbreteau and Ocan Sankur and B. Srivathsan}, editor = {Sergiy Bogomolov and David Parker}, title = {Zone-Based Verification of Timed Automata: Extrapolations, Simulations and What Next?}, booktitle = {Formal Modeling and Analysis of Timed Systems - 20th International Conference, {FORMATS} 2022, Warsaw, Poland, September 13-15, 2022, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13465}, pages = {16--42}, publisher = {Springer}, year = {2022}, url = {https://doi.org/10.1007/978-3-031-15839-1\_2}, doi = {10.1007/978-3-031-15839-1\_2}, PDF = {https://hal.science/hal-03654350} } @inproceedings{DBLP:conf/formats/GoeminneMS22, author = {Aline Goeminne and Nicolas Markey and Ocan Sankur}, editor = {Sergiy Bogomolov and David Parker}, title = {Non-blind Strategies in Timed Network Congestion Games}, booktitle = {Formal Modeling and Analysis of Timed Systems - 20th International Conference, {FORMATS} 2022, Warsaw, Poland, September 13-15, 2022, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {13465}, pages = {183--199}, publisher = {Springer}, year = {2022}, url = {https://arxiv.org/abs/2207.01537}, doi = {10.1007/978-3-031-15839-1\_11}, } @InProceedings{piribauer_et_al:LIPIcs.ICALP.2022.129, author = {Piribauer, Jakob and Sankur, Ocan and Baier, Christel}, title = {{The Variance-Penalized Stochastic Shortest Path Problem}}, booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)}, pages = {129:1--129:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-235-8}, ISSN = {1868-8969}, year = {2022}, volume = {229}, editor = {Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16470}, URN = {urn:nbn:de:0030-drops-164705}, doi = {10.4230/LIPIcs.ICALP.2022.129}, annote = {Keywords: Markov decision process, variance, stochastic shortest path problem}, PDF={https://hal.science/hal-03776449} } @InProceedings{bertrand_et_al:LIPIcs.ICALP.2022.113, author = {Bertrand, Nathalie and Markey, Nicolas and Sankur, Ocan and Waldburger, Nicolas}, title = {{Parameterized Safety Verification of Round-Based Shared-Memory Systems}}, booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)}, pages = {113:1--113:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-235-8}, ISSN = {1868-8969}, year = {2022}, volume = {229}, editor = {Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16454}, URN = {urn:nbn:de:0030-drops-164541}, doi = {10.4230/LIPIcs.ICALP.2022.113}, annote = {Keywords: Verification, Parameterized models, Distributed algorithms} } @inproceedings{DBLP:conf/concur/PiribauerB0S21, author = {Jakob Piribauer and Christel Baier and Nathalie Bertrand and Ocan Sankur}, editor = {Serge Haddad and Daniele Varacca}, title = {Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking}, booktitle = {32nd International Conference on Concurrency Theory, {CONCUR} 2021, August 24-27, 2021, Virtual Conference}, series = {LIPIcs}, volume = {203}, pages = {7:1--7:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2021}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2021.7}, doi = {10.4230/LIPIcs.CONCUR.2021.7}, PDF={https://hal.science/hal-03408379} } @inproceedings{queffelec:hal-03205744, TITLE = {{Planning for Connected Agents in a Partially Known Environment}}, AUTHOR = {Queffelec, Arthur and Sankur, Ocan and Schwarzentruber, François}, URL = {https://hal.archives-ouvertes.fr/hal-03205744}, BOOKTITLE = {{AI 2021 - 34th Canadian Conference on Artificial Intelligence}}, ADDRESS = {Vancouver / Virtual, Canada}, PAGES = {1-23}, YEAR = {2021}, MONTH = May, PDF = {https://hal.archives-ouvertes.fr/hal-03205744/file/halmain.pdf}, HAL_ID = {hal-03205744}, HAL_VERSION = {v1}, } @inproceedings{majith:hal-03153317, TITLE = {{Compositional model checking of a SDN platform}}, AUTHOR = {Majith, Abdul and Sankur, Ocan and Marchand, Herve and Dinh, Thai}, URL = {https://hal.inria.fr/hal-03153317}, BOOKTITLE={{International Conference on the Design of Reliable Communication Networks (DRCN 2021)}}, YEAR = {2021}, MONTH = Feb, PDF = {https://hal.inria.fr/hal-03153317/file/sdn_verif.pdf}, } @article{CQSS-jaamas20, author = {Tristan Charrier and Arthur Queffelec and Ocan Sankur and Fran{\c{c}}ois Schwarzentruber}, title = {Complexity of planning for connected agents}, journal = {Auton. Agents Multi Agent Syst.}, volume = {34}, number = {2}, pages = {44}, year = {2020}, url = {https://doi.org/10.1007/s10458-020-09468-5}, doi = {10.1007/s10458-020-09468-5}, pdf = {https://hal.archives-ouvertes.fr/hal-03003144} } @inproceedings{bertrand:hal-02980833, TITLE = {{Dynamic network congestion games}}, AUTHOR = {Bertrand, Nathalie and Markey, Nicolas and Sadhukhan, Suman and Sankur, Ocan}, URL = {https://hal.archives-ouvertes.fr/hal-02980833}, BOOKTITLE = {{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)}}, ADDRESS = {Goa, India}, YEAR = {2020}, MONTH = Dec, HAL_ID = {hal-02980833}, HAL_VERSION = {v1}, } @inproceedings{JMMNS-formats2020, author="Thierry Jéron, Nicolas Markey, David Mentré, Reiya Noguchi, Ocan Sankur", title="Incremental methods for checking real-time consistency", booktitle="18th International Conference on Formal Modeling and Analysis of Timed Systems, {FORMATS 2020.}", year="2020", abstract="Requirements engineering is a key phase in the development process. Ensuring that requirements are consistent is essential so that they do not conflict and admit implementations. We consider the formal verification of rt-consistency, which imposes that the inevitability of definitive errors of a requirement should be anticipated, and that of partial consistency, which was recently introduced as a more effective check. We generalize and formalize both notions for discrete-time timed automata, develop three incremental algorithms, and present experimental results.", pdf="https://arxiv.org/abs/2007.01014", url="https://www.link.springer.com/book/10.1007/978-3-030-57628-8" } @inproceedings{CQSS-ijcai19, author = {Tristan Charrier and Arthur Queffelec and Ocan Sankur and François Schwarzentruber}, title = {Reachability and Coverage Planning for Connected Agents}, booktitle = {Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, {IJCAI} 2019, Macao, China, August 10-16, 2019}, pages = {144--150}, year = {2019}, crossref = {DBLP:conf/ijcai/2019}, url = {https://doi.org/10.24963/ijcai.2019/21}, doi = {10.24963/ijcai.2019/21}, pdf = "https://hal.archives-ouvertes.fr/hal-02349475v1", } @inproceedings{BBPS-lics19, author={C. Baier and N. Bertrand and J. Piribauer and O. Sankur}, booktitle={2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, title={Long-run Satisfaction of Path Properties}, year={2019}, volume={}, number={}, pages={1-14}, keywords={Markov processes;Probabilistic logic;Frequency measurement;Semantics;Optimization;Standards;Labeling}, doi={10.1109/LICS.2019.8785672}, pdf="https://hal.archives-ouvertes.fr/hal-02349456v1", ISSN={}, month={June}, } @inproceedings{BMRS-cav19, author="Busatto-Gaston, Damien and Monmege, Benjamin and Reynier, Pierre-Alain and Sankur, Ocan", editor="Dillig, Isil and Tasiran, Serdar", title="Robust Controller Synthesis in Timed B{\"u}chi Automata: A Symbolic Approach", booktitle="Computer Aided Verification ({CAV}'19)", year="2019", publisher="Springer International Publishing", address="Cham", pages="572--590", abstract="We solve in a purely symbolic way the robust controller synthesis problem in timed automata with B{\"u}chi acceptance conditions. The goal of the controller is to play according to an accepting lasso of the automaton, while resisting to timing perturbations chosen by a competing environment. The problem was previously shown to be PSPACE-complete using regions-based techniques, but we provide a first tool solving the problem using zones only, thus more resilient to state-space explosion problem. The key ingredient is the introduction of branching constraint graphs allowing to decide in polynomial time whether a given lasso is robust, and even compute the largest admissible perturbation if it is. We also make an original use of constraint graphs in this context in order to test the inclusion of timed reachability relations, crucial for the termination criterion of our algorithm. Our techniques are illustrated using a case study on the regulation of a train network.", isbn="978-3-030-25540-4", url="https://link.springer.com/chapter/10.1007%2F978-3-030-25540-4_33", pdf="https://hal.archives-ouvertes.fr/hal-02264083" } @inproceedings{RSM-cav19, author="Roussanaly, Victor and Sankur, Ocan and Markey, Nicolas", editor="Dillig, Isil and Tasiran, Serdar", title="Abstraction Refinement Algorithms for Timed Automata", booktitle="Computer Aided Verification ({CAV}'19)", year="2019", publisher="Springer International Publishing", address="Cham", pages="22--40", abstract="We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement procedure computes the set of constraints that must be taken into consideration in the abstraction so as to exclude a given spurious counterexample. We implement this idea in two ways: an enumerative algorithm where a lazy abstraction approach is adopted, meaning that possibly different abstract domains are assigned to each exploration node; and a symbolic algorithm where the abstract transition system is encoded with Boolean formulas.", isbn="978-3-030-25540-4", PDF={https://arxiv.org/abs/1905.07365}, url={https://link.springer.com/chapter/10.1007%2F978-3-030-25540-4_2} } @inproceedings{CQSS-aamas19, author = {Charrier, Tristan and Queffelec, Arthur and Sankur, Ocan and Schwarzentruber, François}, title = {Reachability and Coverage Planning for Connected Agents}, booktitle = {Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems}, series = {AAMAS '19}, year = {2019}, isbn = {978-1-4503-6309-9}, location = {Montreal QC, Canada}, pages = {1874--1876}, numpages = {3}, url = {http://dl.acm.org/citation.cfm?id=3306127.3331948}, acmid = {3331948}, publisher = {International Foundation for Autonomous Agents and Multiagent Systems}, address = {Richland, SC}, keywords = {complexity theory and logic, multi-agent planning, paths and connectivity problems}, PDF={https://arxiv.org/abs/1903.04300} } @inproceedings{Baier:2018:SSP:3209108.3209184, author = {Baier, Christel and Bertrand, Nathalie and Dubslaff, Clemens and Gburek, Daniel and Sankur, Ocan}, title = {Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes}, booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science}, series = {LICS '18}, year = {2018}, isbn = {978-1-4503-5583-4}, location = {Oxford, United Kingdom}, pages = {86--94}, numpages = {9}, url = {http://doi.acm.org/10.1145/3209108.3209184}, doi = {10.1145/3209108.3209184}, acmid = {3209184}, publisher = {ACM}, address = {New York, NY, USA}, PDF={https://arxiv.org/abs/1804.11301} } @inproceedings{BRS-kim2017, author="Basset, Nicolas and Raskin, Jean-François and Sankur, Ocan", editor="Aceto, Luca and Bacci, Giorgio and Bacci, Giovanni and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and Mardare, Radu", title="Admissible Strategies in Timed Games", booktitle="Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday", year="2017", publisher="Springer International Publishing", address="Cham", pages="403--425", abstract="In this paper, we study the notion of admissibility in timed games. First, we show that admissible strategies may not exist in timed games with a continuous semantics of time, even for safety objectives. Second, we show that the discrete time semantics of timed games is better behaved w.r.t. admissibility: the existence of admissible strategies is guaranteed in that semantics. Third, we provide symbolic algorithms to solve the model-checking problem under admissibility and the assume-admissible synthesis problem for real-time non-zero sum n-player games for safety objectives.", isbn="978-3-319-63121-9", doi="10.1007/978-3-319-63121-9_20", url="https://doi.org/10.1007/978-3-319-63121-9_20", PDF="https://hal.archives-ouvertes.fr/hal-01515874/document" } @inproceedings{brenguier_et_al:LIPIcs:2017:7806, author ={Romain Brenguier and Arno Pauly and Jean-François Raskin and Ocan Sankur}, title ={{Admissibility in Games with Imperfect Information (Invited Talk)}}, booktitle ={28th International Conference on Concurrency Theory (CONCUR 2017)}, pages ={2:1--2:23}, series ={Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN ={978-3-95977-048-4}, ISSN ={1868-8969}, year ={2017}, volume ={85}, editor ={Roland Meyer and Uwe Nestmann}, publisher ={Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, address ={Dagstuhl, Germany}, URL ={http://drops.dagstuhl.de/opus/volltexte/2017/7806}, URN ={urn:nbn:de:0030-drops-78066}, doi ={10.4230/LIPIcs.CONCUR.2017.2}, annote ={Keywords: Admissibility, non-zero sum games, reactive synthesis, imperfect infor- mation} } @inproceedings{BBGRS-icalp17, author = {Nicolas Basset and Gilles Geeraerts and Jean-François Raskin and Ocan Sankur}, title = {Admissiblity in Concurrent Games}, booktitle = {44th International Colloquium on Automata, Languages, and Programming, {ICALP} 2017, July 10-14, 2017, Warsaw, Poland}, pages = {123:1--123:14}, year = {2017}, url = {https://doi.org/10.4230/LIPIcs.ICALP.2017.123}, doi = {10.4230/LIPIcs.ICALP.2017.123}, timestamp = {Tue, 18 Jul 2017 10:55:26 +0200}, } @inproceedings{ST-tacas17, author = {Ocan Sankur and Jean{-}Pierre Talpin}, title = {An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to {FTSP}}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, {TACAS} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {I}}, pages = {23--40}, year = {2017}, url = {https://doi.org/10.1007/978-3-662-54577-5_2}, PDF = {https://hal.archives-ouvertes.fr/hal-01431472/file/formal.pdf}, doi = {10.1007/978-3-662-54577-5_2}, } @article{Brenguier2017, author="Brenguier, Romain and Raskin, Jean-Fran{ç}ois and Sankur, Ocan", title="Assume-admissible synthesis", journal="Acta Informatica", booktitle="Acta Informatica", year="2017", volume="54", number="1", pages="41--83", abstract="In this paper, we introduce a novel rule for synthesis of reactive systems, applicable to systems made of n components which have each their own objectives. This rule is based on the notion of admissible strategies. We compare this rule with previous rules defined in the literature, and show that contrary to the previous proposals, it defines sets of solutions which are rectangular. This property leads to solutions which are robust and resilient, and allows one to synthesize strategies separately for each agent. We provide algorithms with optimal complexity and also an abstraction framework compatible with the new rule.", issn="1432-0525", doi="10.1007/s00236-016-0273-2", url="http://dx.doi.org/10.1007/s00236-016-0273-2", pdf="https://hal.inria.fr/hal-01373538" } @article{RRS-fmsd17, author="Randour, Mickael and Raskin, Jean-Fran{ç}ois and Sankur, Ocan", title="Percentile queries in multi-dimensional Markov decision processes", journal="Formal Methods in System Design", booktitle="Formal Methods in System Design", year=2017, pages="1--42", issn="1572-8102", doi="10.1007/s10703-016-0262-7", url="http://dx.doi.org/10.1007/s10703-016-0262-7", pdf={http://arxiv.org/abs/1410.4801}, } @inproceedings{brenguier:hal-01373542, TITLE = {Admissibility in Quantitative Graph Games}, AUTHOR = {Brenguier, Romain and Pérez, Guillermo A. and Raskin, Jean-François and Sankur, Ocan}, URL = {https://hal.inria.fr/hal-01373542}, BOOKTITLE = {{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}}, ADDRESS = {Chennai, India}, YEAR = {2016}, MONTH = Dec, HAL_ID = {hal-01373542}, HAL_VERSION = {v1}, } @inproceedings{BCHPRSS-lata16, author="Brenguier, Romain and Clemente, Lorenzo and Hunter, Paul and Pérez, Guillermo A. and Randour, Mickael and Raskin, Jean-Fran{ç}ois and Sankur, Ocan and Sassolas, Mathieu", editor="Dediu, Adrian-Horia and Janou{\v{s}}ek, Jan and Mart{\'i}n-Vide, Carlos and Truthe, Bianca", title="Non-Zero Sum Games for Reactive Synthesis", booktitle="Language and Automata Theory and Applications: 10th International Conference ({LATA 2016}), Prague, Czech Republic, March 14-18, 2016", year="2016", publisher="Springer International Publishing", address="Cham", pages="3--23", volume=9618, series={Lecture Notes in Computer Science}, isbn="978-3-319-30000-9", doi="10.1007/978-3-319-30000-9_1", url="http://dx.doi.org/10.1007/978-3-319-30000-9_1" } @article{Jacobs2016, author={Jacobs, Swen and Bloem, Roderick and Brenguier, Romain and Ehlers, Rüdiger and Hell, Timotheus and Könighofer, Robert and Pérez, Guillermo A. and Raskin, Jean-François and Ryzhyk, Leonid and Sankur, Ocan and Seidl, Martina and Tentrup, Leander and Walker, Adam}, title={The first reactive synthesis competition (SYNTCOMP 2014)}, journal={International Journal on Software Tools for Technology Transfer}, booktitle={International Journal on Software Tools for Technology Transfer}, year="2016", pages="1--24", issn="1433-2787", doi="10.1007/s10009-016-0416-3", url={http://dx.doi.org/10.1007/s10009-016-0416-3}, PDF={http://arxiv.org/abs/1506.08726}, } @inproceedings{BPRS-synt15, author = "Brenguier, Romain and Pérez, Guillermo A. and Raskin, Jean-François and Sankur, Ocan", year = "2016", title = "Compositional Algorithms for Succinct Safety Games", editor = "\v{C}ern\'y, Pavol and Kuncak, Viktor and Parthasarathy, Madhusudan", booktitle = "Proceedings Fourth Workshop on Synthesis {(SYNT'15)}, {San Francisco, CA, USA, 18th July 2015}", series = "Electronic Proceedings in Theoretical Computer Science", volume = "202", publisher = "Open Publishing Association", pages = "98-111", doi = "10.4204/EPTCS.202.7", PDF = {http://arxiv.org/abs/1602.01174}, } @inproceedings{SYNTCOMP2015, author = {Jacobs, Swen and Bloem, Roderick and Brenguier, Romain and Könighofer, Robert and Pérez, Guillermo A. and Raskin, Jean-François and Ryzhyk, Leonid and Sankur, Ocan and Seidl, Martina and Tentrup, Leander and Walker, Adam}, year = {2016}, title = "The Second Reactive Synthesis Competition (SYNTCOMP 2015)", booktitle = "4th Workshop on Synthesis (SYNT 2015)", series = "Electronic Proceedings in Theoretical Computer Science", volume = {202}, publisher = {Open Publishing Association}, pages = "27-57", doi = "10.4204/EPTCS.202.4" } @inproceedings{Sankur-etr15, author={Sankur, Ocan}, title={Controller Synthesis for Timed Systems (Tutorial)}, booktitle={Ecole Temps-Réel ({ETR}'15)}, PDF={http://www.ulb.ac.be/di/verif/sankur/papers/ct-etr15.pdf}, volume={}, year={2015}, publisher={} } @inproceedings{BRS-concur15, author = {Romain Brenguier and Jean-François Raskin and Ocan Sankur}, title = {{Assume-Admissible Synthesis}}, booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)}, pages = {100--113}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-91-0}, ISSN = {1868-8969}, year = {2015}, volume = {42}, editor = {Luca Aceto and David de Frutos Escrig}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, address = {Dagstuhl, Germany}, URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5371}, URN = {urn:nbn:de:0030-drops-53711}, doi = {http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.100}, PDF={http://arxiv.org/abs/1507.00623} } @inproceedings{RRS-cav15, year={2015}, isbn={978-3-319-21689-8}, booktitle={Computer Aided Verification {(CAV 2015)}}, volume={9206}, series={Lecture Notes in Computer Science}, editor={Kroening, Daniel and Păsăreanu, Corina S.}, doi={10.1007/978-3-319-21690-4_8}, title={Percentile Queries in Multi-dimensional Markov Decision Processes}, url={http://dx.doi.org/10.1007/978-3-319-21690-4_8}, pdf={http://arxiv.org/abs/1410.4801}, publisher={Springer International Publishing}, author={Randour, Mickael and Raskin, Jean-François and Sankur, Ocan}, pages={123-139}, language={English} } @inproceedings{Sankur-tacas15, year={2015}, isbn={978-3-662-46680-3}, booktitle={Tools and Algorithms for the Construction and Analysis of Systems {(TACAS'15)}}, volume={9035}, series={Lecture Notes in Computer Science}, editor={Baier, Christel and Tinelli, Cesare}, doi={10.1007/978-3-662-46681-0_48}, title={Symbolic Quantitative Robustness Analysis of Timed Automata}, url={http://dx.doi.org/10.1007/978-3-662-46681-0_48}, publisher={Springer Berlin Heidelberg}, author={Sankur, Ocan}, pages={484-498}, language={English} } @inproceedings{RRS-vmcai2015, author="Randour, Mickael and Raskin, Jean-François and Sankur, Ocan", editor="D'Souza, Deepak and Lal, Akash and Larsen, Kim Guldstrand", title={Variations on the Stochastic Shortest Path Problem}, booktitle={Verification, Model Checking, and Abstract Interpretation: 16th International Conference {(VMCAI 2015)}, Mumbai, India, January 12-14, 2015. Proceedings}, year={2015}, publisher="Springer Berlin Heidelberg", address="Berlin, Heidelberg", pages="1--18", isbn="978-3-662-46081-8", doi="10.1007/978-3-662-46081-8_1", url={http://dx.doi.org/10.1007/978-3-662-46081-8_1}, series={Lecture Notes in Computer Science}, volume={8931}, PDF={http://arxiv.org/abs/1411.0835} } @article{BMS-tcs15, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, title = {Robust Reachability in Timed Automata and Games: A Game-based Approach}, journal = "Theoretical Computer Science", year = {2015}, volume = "563", number = "0", pages = "43 - 74", url = "http://www.sciencedirect.com/science/article/pii/S0304397514006355", PDF = "http://www.ulb.ac.be/di/verif/sankur/papers/BMS-tcs15.pdf" } @inproceedings{RS-fsttcs14, author = {Jean-Francois Raskin and Ocan Sankur}, title = {{Multiple-Environment Markov Decision Processes}}, booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)}, pages = {531--543}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, year = {2014}, volume = {29}, editor = {Venkatesh Raman and S. P. Suresh}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, url = {http://arxiv.org/abs/1405.4733}, } @inproceedings{BPRS-synt14, author = {Brenguier, Romain and Pérez, Guillermo A. and Raskin, Jean-François and Sankur, Ocan}, year = "2014", title = {AbsSynthe: abstract synthesis from succinct safety specifications}, editor = {Chatterjee, Krishnendu and Ehlers, Rüdiger and Jha, Susmit}, booktitle = {{Proceedings 3rd Workshop on} Synthesis (SYNT'14)}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {157}, publisher = {Open Publishing Association}, pages = {100-116}, doi = {10.4204/EPTCS.157.11}, url={http://arxiv.org/abs/1407.5961v1} } @inproceedings{ORS-concur14, year={2014}, isbn={978-3-662-44583-9}, booktitle = {{P}roceedings of the 25th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'14)}, volume={8704}, series={Lecture Notes in Computer Science}, editor={Baldan, Paolo and Gorla, Daniele}, doi={10.1007/978-3-662-44584-6_15}, title={Probabilistic Robust Timed Games}, url={http://dx.doi.org/10.1007/978-3-662-44584-6_15}, publisher={Springer}, author={Oualhadj, Youssouf and Reynier, Pierre-Alain and Sankur, Ocan}, pages={203-217}, language={English}, PDF={http://www.ulb.ac.be/di/verif/sankur/papers/ORS-concur14.pdf} } @article{SBM-ic14, title = "Shrinking timed automata ", journal = "Information and Computation ", volume = "234", number = "0", pages = "107 - 132", year = "2014", issn = "0890-5401", url = "http://www.sciencedirect.com/science/article/pii/S0890540114000030", author = "Ocan Sankur and Patricia Bouyer and Nicolas Markey", PDF = "http://www.ulb.ac.be/di/verif/sankur/papers/SBM-ic14.pdf" } @inproceedings{BMS-rp13, address = {Uppsala, Sweden}, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, booktitle = {{P}roceedings of the 7th {W}orkshop on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'13)}, DOI = {10.1007/978-3-642-41036-9_1}, editor = {Abdulla, Parosh Aziz and Potapov, Igor}, month = sep, pages = {1-18}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Robustness in timed automata}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMS-rp13.pdf}, volume = {8169}, year = {2013}, } @inproceedings{BMS-formats13, address = {Buenos Aires, Argentina}, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, booktitle = {{P}roceedings of the 11th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'13)}, DOI = {10.1007/978-3-642-40229-6_3}, editor = {Braberman, V{\'\i}ctor and Fribourg, Laurent}, month = aug, pages = {31-46}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Robust Weighted Timed Automata and Games}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMS-formats13.pdf}, volume = {8053}, year = {2013}, } @inproceedings{SBMR-concur13, address = {Buenos Aires, Argentina}, author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas and Reynier, Pierre-Alain}, booktitle = {{P}roceedings of the 24th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'13)}, DOI = {10.1007/978-3-642-40184-8_38}, editor = {D'Argenio, Pedro R. and Melgratti, Hern{\'a}n}, month = aug, pages = {546-560}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Robust Controller Synthesis in Timed Automata}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SBMR-concur13.pdf}, volume = {8052}, year = {2013}, } @inproceedings{OS-cav13, address = {Saint Petersburg, Russia}, author = {Sankur, Ocan}, booktitle = {{P}roceedings of the 23th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'13)}, editor = {Sharygina, Natasha and Veith, Helmut}, month = jul, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {8044}, pages = {1006-1012}, title = {Shrinktech: A~Tool for the Robustness Analysis of Timed Automata}, year = {2013}, url={http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/OS-cav13.pdf} } @phdthesis{sankur-phd2013, author = {Sankur, Ocan}, month = jun, school = {Laboratoire Spécification et Vérification, ENS Cachan, France}, type = {Ph.D. thesis}, title = {Robustness in Timed Automata: Analysis, Synthesis, Implementation}, year = {2013}, url={http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/sankur-phd13.pdf} } @inproceedings{BMS-icalp12, address = {Warwick, UK}, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, booktitle = {{P}roceedings of the 39th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'12)~-- {P}art~{II}}, DOI = {10.1007/978-3-642-31585-5_15}, editor = {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew and Wattenhofer, Roger}, month = jul, pages = {128-140}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Robust Reachability in Timed Automata: A~Game-based Approach}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMS-icalp12.pdf}, volume = {7392}, year = {2012}, } @inproceedings{BGS-concur12, address = {Newcastle, UK}, author = {Brenguier, Romain and G{ö}ller, Stefan and Sankur, Ocan}, booktitle = {{P}roceedings of the 23rd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'12)}, DOI = {10.1007/978-3-642-32940-1_12}, editor = {Koutny, Maciej and Ulidowski, Irek}, month = sep, pages = {147-161}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {A~Comparison of Succinctly Represented Finite-State Systems}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGS-concur12.pdf}, volume = {7454}, year = {2012}, } @inproceedings{SBM-fsttcs11, address = {Mumbai, India}, author = {Sankur, Ocan and Bouyer, Patricia and Markey, Nicolas}, booktitle = {{P}roceedings of the 31st {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'11)}, DOI = {10.4230/LIPIcs.FSTTCS.2011.90}, editor = {Chakraborty, Supratik and Kumar, Amit}, month = dec, pages = {90-102}, publisher = {Leibniz-Zentrum f{ü}r Informatik}, series = {Leibniz International Proceedings in Informatics}, title = {Shrinking Timed Automata}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SBM-fsttcs11.pdf}, year = {2011}, } @inproceedings{BLMST-concur11, address = {Aachen, Germany}, author = {Bouyer, Patricia and Larsen, Kim~G. and Markey, Nicolas and Sankur, Ocan and Thrane, Claus}, booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'11)}, DOI = {10.1007/978-3-642-23217-6_6}, editor = {Katoen, Joost-Pieter and K{ö}nig, Barbara}, month = sep, pages = {76-91}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Timed automata can always be made implementable}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BLMST-concur11.pdf}, volume = {6901}, year = {2011}, } @inproceedings{BMS-formats11, address = {Aalborg, Denmark}, author = {Bouyer, Patricia and Markey, Nicolas and Sankur, Ocan}, booktitle = {{P}roceedings of the 9th {I}nternational {C}onference on {F}ormal {M}odelling and {A}nalysis of {T}imed {S}ystems ({FORMATS}'11)}, DOI = {10.1007/978-3-642-24310-3_8}, editor = {Fahrenberg, Uli and Tripakis, Stavros}, month = sep, pages = {97-112}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Robust Model-Checking of Timed Automata via Pumping in Channel Machines}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BMS-formats11.pdf}, volume = {6919}, year = {2011}, } @inproceedings{Sankur-mfcs11, address = {Warsaw, Poland}, author = {Sankur, Ocan}, booktitle = {{P}roceedings of the 36th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'11)}, DOI = {10.1007/978-3-642-22993-0_50}, editor = {Murlak, Filip and Sankowski, Piotr}, month = aug, pages = {556-567}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Untimed Language Preservation in Timed Systems}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/OS-mfcs11.pdf}, volume = {6907}, year = {2011}, } @inproceedings{MSS-stacs10, address = {Nancy, France}, author = {Mathieu, Claire and Sankur, Ocan and Schudy, Warren}, booktitle = {{P}roceedings of the 27th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'10)}, DOI = {10.4230/LIPIcs.STACS.2010.2486}, editor = {Marion, Jean-Yves and Schwentick, Thomas}, month = mar, pages = {573-584}, publisher = {Leibniz-Zentrum f{ü}r Informatik}, series = {Leibniz International Proceedings in Informatics}, title = {Online correlation clustering}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSS-stacs10.pdf}, volume = {5}, year = {2010}, } @mastersthesis{sankur-master, author = {Sankur, Ocan}, month = sep, school={Ecole Normale Supérieure, Paris, France}, type = {{M}aster's thesis}, title = {Model-checking robuste des automates temporisés via les machines {\`a} canaux}, year = {2010}, }
Publications
,
p.
.
Author PDF
[bibtex]