var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=http%3A%2F%2Fwww.cse.chalmers.se%2F%7Epiterman%2Fpublications%2Fpublications.bib&jsonp=1&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=http%3A%2F%2Fwww.cse.chalmers.se%2F%7Epiterman%2Fpublications%2Fpublications.bib&jsonp=1\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=http%3A%2F%2Fwww.cse.chalmers.se%2F%7Epiterman%2Fpublications%2Fpublications.bib&jsonp=1\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
  2. \n
  3. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
  4. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2022\n \n \n (6)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Control and Discovery of Environment Behaviour.\n \n \n \n \n\n\n \n Keegan, M.; Braberman, V.; D'Ippolito, N.; Piterman, N.; and Uchitel, S.\n\n\n \n\n\n\n IEEE Trans. Software Eng., 48(6): 1965–1978. 2022.\n \n\n\n\n
\n\n\n\n \n \n \"Control paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{KBDPU22,\n  author    = {M. Keegan and\n               V.A. Braberman and\n               N. D'Ippolito and\n               N. Piterman and\n               S. Uchitel},\n  title     = {Control and Discovery of Environment Behaviour},\n  journal   = {{IEEE} Trans. Software Eng.},\n  volume    = {48},\n  number    = {6},\n  pages     = {1965--1978},\n  year      = {2022},\n  url_Paper =\t {https://gup.ub.gu.se/file/208369},  \n  keywords = {Model Driven Development,Synthesis,Modelling},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n R-CHECK: A Model Checker for Verifying Reconfigurable MAS.\n \n \n \n \n\n\n \n Alrahman, Y. A.; Azzopardi, S.; and Piterman, N.\n\n\n \n\n\n\n In 21st International Conference on Autonomous Agents and Multiagent Systems, pages 1518–1520, 2022. International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS)\n \n\n\n\n
\n\n\n\n \n \n \"R-CHECK: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{AAP22,\n  author    = {Y. Abd Alrahman and\n               S. Azzopardi and\n               N. Piterman},\n  title     = {{R-CHECK:} {A} Model Checker for Verifying Reconfigurable {MAS}},\n  booktitle = {21st International Conference on Autonomous Agents and Multiagent\n               Systems},\n  pages     = {1518--1520},\n  publisher = {International Foundation for Autonomous Agents and Multiagent Systems\n               {(IFAAMAS)}},\n  year      = {2022},\n  url_Paper =\t {https://gupea.ub.gu.se/bitstream/handle/2077/74141/316806.pdf},  \n  keywords = {Model Checking,Temporal Logic,Modelling,Multi Agents},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Actions over Core-Closed Knowledge Bases.\n \n \n \n \n\n\n \n Cauli, C.; Ortiz, M.; and Piterman, N.\n\n\n \n\n\n\n In 11th International Joint Conference on Automated Reasoning, volume 13385, of Lecture Notes in Computer Science, pages 281–299, 2022. Springer\n \n\n\n\n
\n\n\n\n \n \n \"Actions paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{COP22,\n  author    = {C. Cauli and\n               M. Ortiz and\n               N. Piterman},\n  title     = {Actions over Core-Closed Knowledge Bases},\n  booktitle = {11th International Joint Conference on Automated Reasoning},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {13385},\n  pages     = {281--299},\n  publisher = {Springer},\n  year      = {2022},\n  url_Paper =\t {https://gupea.ub.gu.se/bitstream/handle/2077/72008/main.pdf},  \n  keywords = {Description Logic, Cloud Security},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A PO Characterisation of Reconfiguration.\n \n \n \n \n\n\n \n Alrahman, Y. A.; Martel, M.; and Piterman, N.\n\n\n \n\n\n\n In 19th International Colloquium on Theoretical Aspects of Computing, volume 13572, of Lecture Notes in Computer Science, pages 42–59, 2022. Springer\n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{AMP22,\n  author    = {Y. Abd Alrahman and\n               M. Martel and\n               N. Piterman},\n  title     = {A {PO} Characterisation of Reconfiguration},\n  booktitle = {19th International Colloquium on Theoretical Aspects of Computing},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {13572},\n  pages     = {42--59},\n  publisher = {Springer},\n  year      = {2022},\n  url_Paper =\t {https://gupea.ub.gu.se/bitstream/handle/2077/74182/319965.pdf},  \n  keywords = {Multi Agents,Modelling},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Model Checking Reconfigurable Interacting Systems.\n \n \n \n \n\n\n \n Alrahman, Y. A.; Azzopardi, S.; and Piterman, N.\n\n\n \n\n\n\n In 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, volume 13703, of Lecture Notes in Computer Science, pages 373–389, 2022. Springer\n \n\n\n\n
\n\n\n\n \n \n \"Model paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{AAP22,\n  author    = {Y. Abd Alrahman and\n               S. Azzopardi and\n               N. Piterman},\n  title     = {Model Checking Reconfigurable Interacting Systems},\n  booktitle = {11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {13703},\n  pages     = {373--389},\n  publisher = {Springer},\n  year      = {2022},\n  url_Paper =\t {https://gupea.ub.gu.se/bitstream/handle/2077/74143/319774.pdf},  \n  keywords = {Model Checking,Modelling,Multi Agents,Temporal Logic},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Runtime Verification Meets Controller Synthesis.\n \n \n \n \n\n\n \n Azzopardi, S.; Piterman, N.; and Schneider, G.\n\n\n \n\n\n\n In 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, volume 13701, of Lecture Notes in Computer Science, pages 382–396, 2022. Springer\n \n\n\n\n
\n\n\n\n \n \n \"Runtime paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{APS22,\n  author    = {S. Azzopardi and\n               N. Piterman and\n               G. Schneider},\n  title     = {Runtime Verification Meets Controller Synthesis},\n  booktitle = {11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {13701},\n  pages     = {382--396},\n  publisher = {Springer},\n  year      = {2022},\n  url_Paper =\t {https://gupea.ub.gu.se/bitstream/handle/2077/74142/319773.pdf},  \n  keywords = {Temporal Logic,Runtime Verification,Synthesis},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (8)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Modelling and verification of reconfigurable multi-agent systems.\n \n \n \n \n\n\n \n Alrahman, Y. A.; and Piterman, N.\n\n\n \n\n\n\n Auton. Agents Multi Agent Syst., 35(2): 47. 2021.\n \n\n\n\n
\n\n\n\n \n \n \"Modelling paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{AP21,\n  author    = {Y. Abd Alrahman and\n               N. Piterman},\n  title     = {Modelling and verification of reconfigurable multi-agent systems},\n  journal   = {Auton. Agents Multi Agent Syst.},\n  volume    = {35},\n  number    = {2},\n  pages     = {47},\n  year      = {2021},\n  url_Paper =\t {https://gup.ub.gu.se/file/208622},  \n  keywords = {Model Checking,Modelling,Multi Agents,Temporal Logic},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Incorporating Monitors in Reactive Synthesis Without Paying the Price.\n \n \n \n \n\n\n \n Azzopardi, S.; Piterman, N.; and Schneider, G.\n\n\n \n\n\n\n In 19th International Symposium on Automated Technology for Verification and Analysis, volume 12971, of Lecture Notes in Computer Science, pages 337–353, 2021. Springer\n \n\n\n\n
\n\n\n\n \n \n \"Incorporating paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{APS21,\n  author    = {S. Azzopardi and\n               N. Piterman and\n               G. Schneider},\n  title     = {Incorporating Monitors in Reactive Synthesis Without Paying the Price},\n  booktitle = {19th International Symposium on Automated Technology for Verification and Analysis},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {12971},\n  pages     = {337--353},\n  publisher = {Springer},\n  year      = {2021},\n  url_Paper =\t {https://gupea.ub.gu.se/bitstream/handle/2077/74140/305933.pdf},  \n  keywords = {Temporl Logic,Runtime Verification,Synthesis},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Pre-deployment Security Assessment for Cloud Services Through Semantic Reasoning.\n \n \n \n \n\n\n \n Cauli, C.; Li, M.; Piterman, N.; and Tkachuk, O.\n\n\n \n\n\n\n In 33rd International Conference on Computer Aided Verification, volume 12759, of Lecture Notes in Computer Science, pages 767–780, 2021. Springer\n \n\n\n\n
\n\n\n\n \n \n \"Pre-deployment paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{CLPT21,\n  author    = {C. Cauli and\n               M. Li and\n               N. Piterman and\n               O. Tkachuk},\n  title     = {Pre-deployment Security Assessment for Cloud Services Through Semantic\n               Reasoning},\n  booktitle = {33rd International Conference on Computer Aided Verification},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {12759},\n  pages     = {767--780},\n  publisher = {Springer},\n  year      = {2021},\n  url_Paper =\t {https://gup.ub.gu.se/file/208592},  \n  keywords = {Description Logic, Cloud Security},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning (Extended Abstract).\n \n \n \n \n\n\n \n Cauli, C.; Li, M.; Piterman, N.; and Tkachuk, O.\n\n\n \n\n\n\n In 34th International Workshop on Description Logics, volume 2954, of CEUR Workshop Proceedings, 2021. CEUR-WS.org\n \n\n\n\n
\n\n\n\n \n \n \"Pre-Deployment paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{CLPT21a,\n  author    = {C. Cauli and\n               M. Li and\n               N. Piterman and\n               O. Tkachuk},\n  title     = {Pre-Deployment Security Assessment for Cloud Services through Semantic\n               Reasoning (Extended Abstract)},\n  booktitle = {34th International Workshop on Description Logics},\n  series    = {{CEUR} Workshop Proceedings},\n  volume    = {2954},\n  publisher = {CEUR-WS.org},\n  year      = {2021},\n  url_Paper =\t {},  \n  keywords = {Description Logic, Cloud Security},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Closed- and Open-world Reasoning in DL-Lite for Cloud Infrastructure Security (Extended Abstract).\n \n \n \n \n\n\n \n Cauli, C.; Ortiz, M.; and Piterman, N.\n\n\n \n\n\n\n In Proceedings of the 34th International Workshop on Description Logics, volume 2954, of CEUR Workshop Proceedings, 2021. CEUR-WS.org\n \n\n\n\n
\n\n\n\n \n \n \"Closed- paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{COP21a,\n  author    = {C. Cauli and\n               M. Ortiz and\n               N. Piterman},\n  title     = {Closed- and Open-world Reasoning in DL-Lite for Cloud Infrastructure\n               Security (Extended Abstract)},\n  booktitle = {Proceedings of the 34th International Workshop on Description Logics},\n  series    = {{CEUR} Workshop Proceedings},\n  volume    = {2954},\n  publisher = {CEUR-WS.org},\n  year      = {2021},\n  url_Paper =\t {},  \n  keywords = {Description Logic, Cloud Security},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Closed- and Open-world Reasoning in DL-Lite for Cloud Infrastructure Security.\n \n \n \n \n\n\n \n Cauli, C.; Ortiz, M.; and N.Piterman\n\n\n \n\n\n\n In Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, pages 174–183, 2021. \n \n\n\n\n
\n\n\n\n \n \n \"Closed- paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{COP21,\n  author    = {C. Cauli and\n               M. Ortiz and\n               N.Piterman},\n  title     = {Closed- and Open-world Reasoning in DL-Lite for Cloud Infrastructure\n               Security},\n  booktitle = {Proceedings of the 18th International Conference on Principles of\n               Knowledge Representation and Reasoning},\n  pages     = {174--183},\n  year      = {2021},\n  url_Paper =\t {https://gup.ub.gu.se/file/208720},  \n  keywords = {Description Logic, Cloud Security},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesis of Run-To-Completion Controllers for Discrete Event Systems.\n \n \n \n \n\n\n \n Abd Alrahman, Y.; Braberman, V. A.; D'Ippolito, N.; Piterman, N.; and Uchitel, S.\n\n\n \n\n\n\n . May 2021.\n \n\n\n\n
\n\n\n\n \n \n \"Synthesis paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 10 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{ABDPU21,\n  author    = {Y. {Abd Alrahman} and\n               V. A. Braberman and\n               N. D'Ippolito and\n               N. Piterman and\n               S. Uchitel},\n  title = {Synthesis of Run-To-Completion Controllers for Discrete Event Systems}, \n  booktitle = {American Control Conference}, \n  OPTpages = {}, \n  year = {2021}, \n  OPTseries = {}, \n  address = {New Orleans, Louisiana, USA}, \n  month = {May}, \n  publisher = {{IEEE} press}, \n  year = {2021}, \n  url_Paper =\t {https://gup.ub.gu.se/file/208493},  \n  keywords = {Games,Synthesis,Model Driven Development},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Control and Discovery of Environment Behaviour.\n \n \n \n \n\n\n \n Keegan, M.; Braberman, V.; D'Ippolito, N.; Piterman, N.; and Uchitel, S.\n\n\n \n\n\n\n IEEE Transactions on Software Engineering. 2021.\n \n\n\n\n
\n\n\n\n \n \n \"Control paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@ARTICLE{KBDPU21,\n  author =       {M. Keegan and V. Braberman and N. D'Ippolito and N. Piterman and S. Uchitel},\n  title =\t {Control and Discovery of Environment Behaviour},\n  journal =      {IEEE Transactions on Software Engineering},\n  OPTvolume =    {82},\n  OPTnumber =    {2}, \n  OPTpages =\t {420-452},\n  year =\t {2021},\n  publisher = {IEEE Press},\n  url_Paper =\t {https://gup.ub.gu.se/file/208369},\n  keywords = {Games,Synthesis,Model Driven Development},\n}\n\n\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Reconfigurable Interaction for MAS Modelling.\n \n \n \n \n\n\n \n Abd Alrahman, Y.; Perelli, G.; and Piterman, N.\n\n\n \n\n\n\n In Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems, pages 7-15, 2020. International Foundation for Autonomous Agents and Multiagent Systems\n \n\n\n\n
\n\n\n\n \n \n \"Reconfigurable paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 29 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{APP20,\n  author    = {Y. {Abd Alrahman} and\n               G. Perelli and\n               N. Piterman},\n  title     = {Reconfigurable Interaction for {MAS} Modelling},\n  booktitle = {Proceedings of the 19th International Conference on Autonomous Agents\n               and Multiagent Systems},\n  pages     = {7-15},\n  publisher = {International Foundation for Autonomous Agents and Multiagent Systems},\n  year      = {2020},\n  url_Paper = {2020/APP20.pdf},\n  keywords = {Automata,Model Checking,Multi Agents},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2019\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Combinations of Qualitative Winning for Stochastic Parity Games.\n \n \n \n\n\n \n Chatterjee, K.; and Piterman, N.\n\n\n \n\n\n\n In 30th International Conference on Concurrency Theory, of LIPIcs, pages 229-246, Amsterdam, Netherlands, August 2019. Schloss Dagstuhl\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@INPROCEEDINGS{CP19,\n  author    = {K. Chatterjee and\n               N. Piterman},\n  title     = {Combinations of Qualitative Winning for Stochastic Parity Games},\n  booktitle = {30th International Conference on Concurrency Theory},\n  pages     = {229-246},\n  year      = {2019},\n  series    = {LIPIcs},\naddress = {Amsterdam, Netherlands},\n   month = {August},\n  publisher = {Schloss Dagstuhl},\n  opturl_Paper = {2019/CP19.pdf},\n  keywords = {Games},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Environmentally-Friendly GR(1) Synthesis.\n \n \n \n \n\n\n \n Majumdar, R.; Piterman, N.; and Schmuck, A.\n\n\n \n\n\n\n In 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 11428, of Lecture Notes in Computer Science, pages 229-246, Prague, Czech Republic, April 2019. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Environmentally-Friendly paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 11 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@INPROCEEDINGS{MPS19,\n  author    = {R. Majumdar and\n               N. Piterman and\n               A.-K. Schmuck},\n  title     = {Environmentally-Friendly {GR(1)} Synthesis},\n  booktitle = {25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},\n  pages     = {229-246},\n  year      = {2019},\n  series    = {Lecture Notes in Computer Science},\n  volume    = {11428},\naddress = {Prague, Czech Republic},\n   month = {April},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2019/MPS19.pdf},\n  keywords = {Games,Synthesis},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Using State Space Exploration to Determine How Gene Regulatory Networks Constrain Mutation Order in Cancer Evolution.\n \n \n \n\n\n \n Clarke, M.; Woodhouse, S.; Piterman, N.; Hall, B.; and Fisher, J.\n\n\n \n\n\n\n In Automated Reasoning for Systems Biology and Medicine, volume 30, of Computational Biology, pages 133-153. © Springer-Verlag, 2019.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@INCOLLECTION{CWPHF19,\n  author    = {M.A. Clarke and\n               S. Woodhouse and\n               N. Piterman and\n               B.A. Hall and\n               J. Fisher},\n  title     = {Using State Space Exploration to Determine How Gene Regulatory Networks\n               Constrain Mutation Order in Cancer Evolution},\n  booktitle = {Automated Reasoning for Systems Biology and Medicine},\n  pages     = {133-153},\n  year      = {2019},\n  series    = {Computational Biology},\n  volume    = {30},\n  publisher = {&copy; Springer-Verlag},\n  keywords = {Executable Biology},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A Toolbox for Discrete Modelling of Cell Signalling Dynamics.\n \n \n \n \n\n\n \n Paterson, Y.; Shorthouse, D.; Pleijzier, M.; Piterman, N.; Bendtsen, C.; Hall, B.; and Fisher, J.\n\n\n \n\n\n\n Integrative Biology. 2018.\n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@ARTICLE{PSPPBHF18,\n  author =       {Y. Paterson and D. Shorthouse and M. Pleijzier and N. Piterman and C. Bendtsen and B.A. Hall and J. Fisher},\n  title = \t {A Toolbox for Discrete Modelling of Cell Signalling Dynamics},\n  journal =      {Integrative Biology},\n  OPTvolume =    {82},\n  OPTnumber =    {2}, \n  OPTpages = \t {420-452},\n  year = \t {2018},\n  OPTpublisher = {ACM},\n  url_Paper = \t {https://lra.le.ac.uk/bitstream/2381/42024/2/finalSub.pdf},\n  keywords = {Executable Biology},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2017\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Obligation Blackwell Games and p-Automata.\n \n \n \n \n\n\n \n Chatterjee, K.; and Piterman, N.\n\n\n \n\n\n\n Journal of Symbolic Logic, 82(2): 420-452. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"Obligation paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@article{CP17,\n  author =       {K. Chatterjee and N. Piterman},\n  title = \t {Obligation Blackwell Games and p-Automata},\n  journal =      {Journal of Symbolic Logic},\n  volume =    {82},\n  number =    {2}, \n  pages = \t {420-452},\n  year = \t {2017},\n  OPTpublisher = {ACM},\n  url_Paper = \t {2017/CP17.pdf},\n  keywords = {Automata,Games},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems.\n \n \n \n \n\n\n \n Cook, B.; Khlaaf, H.; and Piterman, N.\n\n\n \n\n\n\n Journal of the ACM. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"Verifying paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@article{CKP17,\n  author =       {B. Cook and H. Khlaaf and N. Piterman},\n  title = \t {Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems},\n  journal =      {Journal of the ACM},\n  OPTvolume =    {64},\n  OPTnumber =    {2}, \n  OPTpages = \t {15},\n  year = \t {2017},\n  publisher = {ACM},\n  url_Paper = \t {2017/CKP17.pdf},\n  keywords = {Model Checking,Temporal Logic},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Bringing LTL Model Checking to Biologists.\n \n \n \n \n\n\n \n Ahmed, Z.; Benque, D.; Berezin, S.; Dahl, A.; Fisher, J.; Hall, B.; Ishtiaq, S.; Nanavati, J.; Piterman, N.; Riechert, M.; and Skoblov, N.\n\n\n \n\n\n\n In 18th International Conference on Verification, Model Checking, and Abstract Interpretation, volume 10145, of Lecture Notes in Computer Science, pages 1-13, 2017. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Bringing paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@inproceedings{ABBDFHINPRS17,\n  author    = {Z. Ahmed and\n               D. Benque and\n               S. Berezin and\n               A.C.E. Dahl and\n               J. Fisher and\n               B.A. Hall and\n               S. Ishtiaq and\n               J. Nanavati and\n               N. Piterman and\n               M. Riechert and\n               N. Skoblov},\n  title     = {Bringing {LTL} Model Checking to Biologists},\n  booktitle = {18th International Conference on Verification, Model Checking, and Abstract Interpretation},\n  pages     = {1-13},\n  year      = {2017},\n  series    = {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  volume    = {10145},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {https://lra.le.ac.uk/bitstream/2381/39503/2/cav2016.pdf},\n  keywords = {Executable Biology},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Interaction Models and Automated Control under Partial Observable Environments.\n \n \n \n \n\n\n \n Ciolek, D.; D'Ippolito, N.; Braberman, V.; Piterman, N.; and Uchitel, S.\n\n\n \n\n\n\n IEEE Transactions on Software Engineering, 43(1): 19-33. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"Interaction paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@Article{CBDPU17,\n  author = \t {D. Ciolek and N. D'Ippolito and V. Braberman and N. Piterman and S. Uchitel},\n  title = \t {Interaction Models and Automated Control under Partial Observable Environments},\n  journal =   {IEEE Transactions on Software Engineering},\n  year = {2017},\n  volume = {43},\n  number = {1},\n  pages =  {19-33},\n  url_Paper = {2017/CBDPU17.pdf},\n  keywords = {Synthesis,Games,Model Driven Development},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2016\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Static Analysis of Parity Games: Alternating Reachability Under Parity.\n \n \n \n \n\n\n \n Huth, M.; Kuo, J.; and Piterman, N.\n\n\n \n\n\n\n In Semantics, Logic, and Calculi - Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of their 60th Birthdays, volume 9560, of Lecture Notes in Computer Science, pages 159-177. © Springer-Verlag, 2016.\n \n\n\n\n
\n\n\n\n \n \n \"Static paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InCollection{HKP16,\n  author = \t {M. Huth and J.H. Kuo and N. Piterman},\n  title = \t {Static Analysis of Parity Games: Alternating Reachability Under Parity},\n  booktitle = \t {Semantics, Logic, and Calculi - Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of their 60th Birthdays},\n  pages = \t {159-177},\n  year = \t {2016},\n  volume = \t {9560},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = \t {2016/HKP16.pdf},\n  keywords = {Games,Static Analysis},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Safety Verification of Piecewise-Deterministic Markov Processes.\n \n \n \n \n\n\n \n Wisniewski, R.; Sloth, C.; Bujorianu, M.; and Piterman, N.\n\n\n \n\n\n\n In 19th International Conference on Hybrid Systems: Computation and Control, pages 257-266, 2016. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Safety paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{WSBP16,\n  author =       {R. Wisniewski and C. Sloth and M.L. Bujorianu and N. Piterman},\n  title = \t {Safety Verification of Piecewise-Deterministic Markov Processes},\n  booktitle = {19th International Conference on Hybrid Systems: Computation and Control},\n  pages = \t {257-266},\n  OPTvolume =       {},\n  year = \t {2016},\n  publisher = {ACM},\n  url_Paper = \t {2016/WSBP16.pdf},\n  keywords = {Hybrid Systems},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Finding Recurrent Sets with Backward Analysis and Trace Partitioning.\n \n \n \n \n\n\n \n Bakhirkin, A.; and Piterman, N.\n\n\n \n\n\n\n In 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 9636, of Lecture Notes in Computer Science, pages 17-35, 2016. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Finding paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{BP16,\n  author =       {A. Bakhirkin and N. Piterman},\n  title = \t {Finding Recurrent Sets with Backward Analysis and Trace Partitioning},\n  booktitle = {22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems},\n  pages = \t {17-35},\n  volume =       {9636},\n  year = \t {2016},\n  series = {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = \t {https://lra.le.ac.uk/bitstream/2381/36303/2/paper_30.pdf},\n  OPTurl_Link = \t {},\n  keywords = {Static Analysis},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n T2: Temporal Property Verification.\n \n \n \n \n\n\n \n Brockschmidt, M.; Cook, B.; Ishtiaq, S.; Khlaaf, H.; and Piterman, N.\n\n\n \n\n\n\n In 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 9636, of Lecture Notes in Computer Science, pages 387-393, 2016. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"T2: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{BCIKP16,\n  author =       {M. Brockschmidt and B. Cook and S. Ishtiaq and H. Khlaaf and N. Piterman},\n  title = \t {T2: Temporal Property Verification},\n  booktitle = {22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems},\n  pages = \t {387-393},\n  volume =       {9636},\n  year = \t {2016},\n  publisher = {&copy; Springer-Verlag},\n  series = {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  url_Paper = \t {2016/BCIKP16.pdf},\n  keywords = {Model Checking,Temporal Logic},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2015\n \n \n (12)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n 11th International Haifa Verification Conference.\n \n \n \n\n\n \n Piterman, N.,\n editor.\n \n\n\n \n\n\n\n Volume 9434, of Lecture Notes in Computer Science.© Springer-Verlag. Haifa, Israel, November 2015.\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@proceedings{Pit15,\n  proceedings      = {},\n  editor    = {N. Piterman},\n  title     = {11th International Haifa Verification Conference},\n  series = {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  volume    = {9434},\n  publisher = {&copy; Springer-Verlag},\nyear      = {2015},\nmonth = {November},\naddress = {Haifa, Israel},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Recursive Probabilistic Temporal Logic.\n \n \n \n \n\n\n \n Castro, P.; Kilmurray, C.; and Piterman, N.\n\n\n \n\n\n\n In 17th International Conference on Formal Methods and Softare Engineering, volume 9407, of Lecture Notes in Computer Science, 2015. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@INPROCEEDINGS{CKP15b,\n  author =       {P. Castro and C. Kilmurray and N. Piterman},\n  title = \t {A Recursive Probabilistic Temporal Logic},\n  booktitle = {17th International Conference on Formal Methods and Softare Engineering},\n  OPTpages = \t {},\n  year = \t {2015},\n  volume = {9407},\n  publisher = {&copy; Springer-Verlag},\n  series = {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  url_Paper = \t {2015/CKP15b},\n  keywords = {Automata,Games,Temporal Logic},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Emergent Stem Cell Homeostasis in C. elegans germline Revealed by Hybrid Modelling.\n \n \n \n \n\n\n \n Hall, B.; Piterman, N.; Hajnal, A.; and Fisher, J.\n\n\n \n\n\n\n The Biophysical Journal. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"Emergent paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{HPHF15,\n  author = \t {B.A. Hall and N. Piterman and A. Hajnal and J. Fisher},\n  title        = {Emergent Stem Cell Homeostasis in C. elegans germline Revealed by Hybrid Modelling},\n  journal      = {The Biophysical Journal},\n  year         = {2015},\n  OPTvolume = \t {},\n  OPTpages = {},\n  url_Paper = {https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/Biophys_J_Jul15.pdfja},\n  keywords = {Executable Biology,Biology},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Forward Analysis for Recurrent Sets.\n \n \n \n \n\n\n \n Bakhirkin, A.; Berdine, J.; and Piterman, N.\n\n\n \n\n\n\n In 22nd International Static Analysis Symposium, of Lecture Notes in Computer Science, San Malo, France, 2015. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{BBP15,\n  author = {A. Bakhirkin and J. Berdine and N. Piterman},\n  title =        {A Forward Analysis for Recurrent Sets},\n  booktitle = {22nd International Static Analysis Symposium},\n  OPTpages = {},\n  year = {2015},\n  OPTvolume = {},\n  address = {San Malo, France},\n  publisher = {&copy; Springer-Verlag},\n  series = {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  keywords = {Model Checking, Static Analysis},\n  url_Paper = {2015/BBP15.pdf},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data.\n \n \n \n \n\n\n \n Woodhouse, S.; Piterman, N.; Koskal, A.; and Fisher, J.\n\n\n \n\n\n\n In 27th International Conference on Computer Aided Verification, volume 9206, of Lecture Notes in Computer Science, 2015. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Synthesising paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{WPKF15,\n  author =       {S. Woodhouse and N. Piterman and A.S. Koskal and J. Fisher},\n  title = \t {Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data},\n  booktitle = {27th International Conference on Computer Aided Verification},\n  OPTpages = \t {},\n  year = \t {2015},\n  publisher = {&copy; Springer-Verlag},\n  series = {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  volume = \t {9206},\n  url_Paper = \t {2015/WPKF15.pdf},\n  keywords = {Executable Biology,Synthesis},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n On Automation of CTL* Verification for Infinite-State Systems.\n \n \n \n \n\n\n \n Cook, B.; Khlaaf, H.; and Piterman, N.\n\n\n \n\n\n\n In 27th International Conference on Computer Aided Verification, volume 9206, of Lecture Notes in Computer Science, 2015. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"On paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{CKP15c,\n  author =       {B. Cook and H. Khlaaf and N. Piterman},\n  title = \t {On Automation of CTL* Verification for Infinite-State Systems},\n  booktitle = {27th International Conference on Computer Aided Verification},\n  OPTpages = \t {},\n  year = \t {2015},\n  publisher = {&copy; Springer-Verlag},\n  series = {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  volume = \t {9206},\n  url_Paper = \t {2015/CKP15c},\n  keywords = {Model Checking,Temporal Logic},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Timing Semantics for Abstraction and Execution of Synthesized High-Level Robot Control.\n \n \n \n \n\n\n \n Raman, V.; Piterman, N.; Finucane, C.; and Kress-Gazit, H.\n\n\n \n\n\n\n IEEE Transactions on Robotics. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"Timing paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{RPFK15,\n  author = \t {V. Raman and N. Piterman and C. Finucane and H. Kress-Gazit},\n  title        = {Timing Semantics for Abstraction and Execution of Synthesized High-Level Robot Control},\n  journal      = {IEEE Transactions on Robotics},\n  year         = {2015},\n  OPTvolume = \t {},\n  OPTpages = {8190},\n  url_Paper = {2015/RPFK14.pdf},\n  keywords = {Games,Synthesis},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Drug Target Optimization in Chronic Myeloid Leukemia Using Innovative Computational Platform.\n \n \n \n \n\n\n \n Chuang, R.; Hall, B.; Benque, D.; Cook, B.; Ishtiaq, S.; Piterman, N.; Taylor, A.; Vardi, M.; Koschmieder, S.; Gottgens, B.; and Fisher, J.\n\n\n \n\n\n\n Scientific Reports, 5: 8190. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"Drug paper\n  \n \n \n \"Drug link\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{CHBCIPTVKGF15,\n  author = \t {R. Chuang and B.A. Hall and D. Benque and B. Cook and S. Ishtiaq and N. Piterman and A. Taylor and M.Y. Vardi and S. Koschmieder and B. Gottgens and J. Fisher},\n  title        = {Drug Target Optimization in Chronic Myeloid Leukemia Using Innovative Computational Platform},\n  journal      = {Scientific Reports},\n  year         = {2015},\n  volume = \t {5},\n  pages = {8190},\n  url_Paper = {http://www.nature.com/srep/2015/150203/srep08190/pdf/srep08190.pdf},\n  url_Link = {http://www.nature.com/srep/2015/150203/srep08190/full/srep08190.html},\n  keywords = {Biology,Executable Biology},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Decoding the Transcriptional Program for Blood Development from Single Cell Gene Expression Measurements.\n \n \n \n \n\n\n \n Moignard, V.; Woodhouse, S.; Haghverdi, L.; Lilly, J.; Tanaka, Y.; Wilkinson, A.; Buettner, F.; Macaulay, I.; Jawaid, W.; Diamanti, E.; Nishikawa, S.; Piterman, N.; Kouskoff, V.; Theis, F.; Fisher, J.; and Gottgens, B.\n\n\n \n\n\n\n Nature Biotechnology. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"Decoding link\n  \n \n \n \"Decoding paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@Article{MWHLTWBMJDNPKTFG15,\n  author = \t {V. Moignard and S. Woodhouse and L. Haghverdi and J. Lilly and Y. Tanaka and A.C. Wilkinson and F. Buettner and I.C. Macaulay and W. Jawaid and E. Diamanti and S.-I. Nishikawa and N. Piterman and V. Kouskoff and F.J. Theis and J. Fisher and B. Gottgens},\n  title        = {Decoding the Transcriptional Program for Blood Development from Single Cell Gene Expression Measurements},\n  journal      = {Nature Biotechnology},\n  year         = {2015},\n  OPTvolume = \t {},\n  OPTnumber = {},\n  url_Link = {http://www.nature.com/nbt/journal/vaop/ncurrent/full/nbt.3154.html},\n  url_Paper = {http://www.nature.com/nbt/journal/vaop/ncurrent/pdf/nbt.3154.pdf},\n  keywords = {Biology,Executable Biology,Synthesis},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Rabin Index of Parity Games: Its Complexity and Approximation.\n \n \n \n \n\n\n \n Huth, M.; Kuo, J.; and Piterman, N.\n\n\n \n\n\n\n Information and Computation. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"The paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@Article{HKP15,\n  author = \t {M. Huth and J.H. Kuo and N. Piterman},\n  title        = {The Rabin Index of Parity Games: Its Complexity and Approximation},\n  journal      = {Information and Computation},\n  year         = {2015},\n  OPTvolume = \t {},\n  OPTnumber = {},\n  url_Paper = {2015/HKP15.pdf},\n  keywords = {Games},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Fairness for Infinite-State Systems.\n \n \n \n \n\n\n \n Cook, B.; Khlaaf, H.; and Piterman, N.\n\n\n \n\n\n\n In 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 9035, of Lecture Notes in Computer Science, pages 384-398, 2015. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Fairness paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{CKP15a,\n  author =       {B. Cook and H. Khlaaf and N. Piterman},\n  title = \t {Fairness for Infinite-State Systems},\n  booktitle = {21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems},\n  pages = \t {384-398},\n  year = \t {2015},\n  publisher = {&copy; Springer-Verlag},\n  series = {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  volume = {9035},\n  url_Paper = \t {2015/CKP15a.pdf},\n  keywords = {Model Checking,Temporal Logic},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics.\n \n \n \n \n\n\n \n Castro, P.; Kilmurray, C.; and Piterman, N.\n\n\n \n\n\n\n In 32nd Symposium on Theoretical Aspects of Computer Science, of LIPIcs, 2015. Schloss Dagstuhl\n \n\n\n\n
\n\n\n\n \n \n \"Tractable paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{CKP15,\n  author =       {P. Castro and C. Kilmurray and N. Piterman},\n  title = \t {Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics},\n  booktitle = {32nd Symposium on Theoretical Aspects of Computer Science},\n  OPTpages = \t {},\n  year = \t {2015},\n  publisher = {Schloss Dagstuhl},\n  series = {LIPIcs},\n  url_Paper = \t {2015/CKP15.pdf},\n  keywords = {Automata,Games,Temporal Logic},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2014\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Modelling Biology - Working through (in)-Stabilities and Frictions.\n \n \n \n \n\n\n \n Taylor, A.; Fisher, J.; Cook, B.; Ishtiaq, S.; and Piterman, N.\n\n\n \n\n\n\n Computational Culture, 4. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"Modelling link\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@Article{TFCIP14,\n  author = \t {A. Taylor and J. Fisher and B. Cook and S. Ishtiaq and N. Piterman},\n  title        = {Modelling Biology - Working through (in)-Stabilities and Frictions},\n  journal      = {Computational Culture},\n  year         = {2014},\n  volume = \t {4},\n  url_Link = {http://computationalculture.net/article/modelling-biology},\n  keywords = {Executable Biology},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Faster Temporal Reasoning for Infinite-State Programs.\n \n \n \n \n\n\n \n Cook, B.; Khlaaf, H.; and Piterman, N.\n\n\n \n\n\n\n In 14th conference on Formal Methods in Computer-Aided Design, pages 75-82, Lausanne, Switzerland, 2014. © ieee press\n \n\n\n\n
\n\n\n\n \n \n \"Faster paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{CKP14,\n  author = {B. Cook and H. Khlaaf and N. Piterman},\n  title =        {Faster Temporal Reasoning for Infinite-State Programs},\n  booktitle = {14th conference on Formal Methods in Computer-Aided Design},\n  pages = {75-82},\n  year = {2014},\n  address = {Lausanne, Switzerland},\n  publisher = {&copy; ieee press},\n  keywords = {Model Checking},\n  url_Paper = {2014/CKP14.pdf},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Backward Analysis via Over-Approximate Abstraction and Under-Approximate Subtraction.\n \n \n \n \n\n\n \n Bakhirkin, A.; Berdine, J.; and Piterman, N.\n\n\n \n\n\n\n In 21st International Static Analysis Symposium, volume 8723, of Lecture Notes in Computer Science, pages 34-50, Munich, Germany, 2014. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Backward paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{BBP14,\n  author = {A. Bakhirkin and J. Berdine and N. Piterman},\n  title =        {Backward Analysis via Over-Approximate Abstraction\n                  and Under-Approximate Subtraction},\n  booktitle = {21st International Static Analysis Symposium},\n  pages = {34-50},\n  year = {2014},\n  volume = {8723},\n  address = {Munich, Germany},\n  publisher = {&copy; Springer-Verlag},\n  series = {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  keywords = {Model Checking, Static Analysis},\n  url_Paper = {2014/BBP14.pdf},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Controllability in Partial and Uncertain Environments.\n \n \n \n \n\n\n \n D'Ippolito, N.; Braberman, V.; Piterman, N.; and Uchitel, S.\n\n\n \n\n\n\n In 14th International Conference on Application of Concurrency to System Design, pages 52-61, Tunis, Tunisia, 2014. © ieee press\n \n\n\n\n
\n\n\n\n \n \n \"Controllability paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{DBPU14,\n  author = {N. D'Ippolito and V. Braberman and N. Piterman and S. Uchitel},\n  title = {Controllability in Partial and Uncertain Environments},\n  booktitle = {14th International Conference on Application of Concurrency to System Design},\n  pages = {52-61},\n  year = {2014},\n  address = {Tunis, Tunisia},\n  publisher = {&copy; ieee press},\n  keywords = {Synthesis},\n  url_Paper = {2014/DBPU14.pdf},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Finding Instability in Biological Models.\n \n \n \n \n\n\n \n Cook, B.; Fisher, J.; Hall, B.; Ishtiaq, S.; Juniwal, G.; and Piterman, N.\n\n\n \n\n\n\n In 26th International Conference on Computer Aided Verification, volume 8559, of Lecture Notes in Computer Science, pages 358-372, Vienna, Austria, 2014. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Finding paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{CFHIJP14,\n  author = {B. Cook and J. Fisher and B.A. Hall and S. Ishtiaq and G. Juniwal and N. Piterman},\n  title = {Finding Instability in Biological Models},\n  booktitle = {26th International Conference on Computer Aided Verification},\n  pages = {358-372},\n  year = {2014},\n  volume = {8559},\n  address = {Vienna, Austria},\n  publisher = {&copy; Springer-Verlag},\n  series = {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  keywords = {Executable Biology},\n  url_Paper = {2014/BDPU14.pdf},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2013\n \n \n (10)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Tools and Algorithms for the Construction and Analysis of Systems, 19th International Conference.\n \n \n \n \n\n\n \n Piterman, N.; and Smolka, S.,\n editors.\n \n\n\n \n\n\n\n Volume 7795 of Lecture Notes in Computer Science© Springer-Verlag, 2013.\n \n\n\n\n
\n\n\n\n \n \n \"Tools link\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@Book{PS13,\n  editor = \t {N. Piterman and S.A. Smolka},\n  title = \t {Tools and Algorithms for the Construction and Analysis of Systems, 19th International Conference},\n  year = \t 2013,\n  volume = \t {7795},\n  publisher = \t {&copy; Springer-Verlag},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  url_Link = {http://www.springerlink.com/content/978-3-642-36741-0/},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesis from Temporal Specifications: New Applications in Robotics and Model-Driven Development.\n \n \n \n \n\n\n \n Piterman, N.\n\n\n \n\n\n\n In 38th International Symposium on Mathematical Foundations of Computer Science, volume 8087, of Lecture Notes in Computer Science, pages 45-49, Klosterneuburg, Austria, 2013. &Copy; Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Synthesis paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@inproceedings{Pit13,\n  author    = {N. Piterman},\n  title     = {Synthesis from Temporal Specifications: New Applications\n               in Robotics and Model-Driven Development},\n  year      = {2013},\n  pages     = {45-49},\n  booktitle     = {38th International Symposium on Mathematical Foundations of Computer Science},\n  publisher = {{&Copy; Springer-Verlag}},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  volume    = {8087},\n  url_Paper = {2013/Pit13.pdf},\n  address = {Klosterneuburg, Austria},\n  keywords = {Synthesis},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Model-Checking Signal Transduction Networks through Decreasing Reachability Sets.\n \n \n \n \n\n\n \n Claessen, K.; Fisher, J.; Ishtiaq, S.; Piterman, N.; and Wang, Q.\n\n\n \n\n\n\n In The 25th Conference on Computer Aided Verification, volume 8044, of Lecture Notes in Computer Science, pages 85-100, St Petersburg, Russia, 2013. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Model-Checking paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{CFIPW13,\n  author = \t {K. Claessen and J. Fisher and S. Ishtiaq and N. Piterman and Q. Wang},\n  title = \t {Model-Checking Signal Transduction Networks through Decreasing Reachability Sets},\n  booktitle = {The 25th Conference on Computer Aided Verification},\n  pages = \t {85-100},\n  year = \t {2013},\n  volume = \t {8044},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {St Petersburg, Russia},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2013/CFIPW13.pdf},\n  keywords = {Executable Biology},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Controller synthesis: From modelling to enactment.\n \n \n \n \n\n\n \n Braberman, V.; D'Ippolito, N.; Piterman, N.; Sykes, D.; and Uchitel, S.\n\n\n \n\n\n\n In 35th International Conference on Software Engineering, pages 1347-1350, San Francisco, CA, USA, 2013. © ieee press\n \n\n\n\n
\n\n\n\n \n \n \"Controller paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{BDPSU13,\n  author = {V. Braberman and N. D'Ippolito and N. Piterman and D. Sykes and S. Uchitel},\n  title = {Controller synthesis: From modelling to enactment},\n  booktitle = {35th International Conference on Software Engineering},\n  pages = {1347-1350},\n  year = {2013},\n  address = {San Francisco, CA, USA},\n  publisher = {&copy; ieee press},\n  keywords = {Synthesis},\n  url_Paper = {2013/BDPSU13.pdf},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Provably Correct Continuous Control for High-Level Robot Behaviors with Actions of Arbitrary Execution Durations.\n \n \n \n \n\n\n \n Raman, V.; Piterman, N.; and Kress-Gazit, H.\n\n\n \n\n\n\n In IEEE International Conference on Robotics and Automation, pages 4075-4081, Karlsruhe, Germany, 2013. © ieee press\n \n\n\n\n
\n\n\n\n \n \n \"Provably paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{RPK13,\n  author = {V. Raman and N. Piterman and H. Kress-Gazit},\n  title = {Provably Correct Continuous Control for High-Level Robot Behaviors with Actions of Arbitrary Execution Durations},\n  booktitle = {IEEE International Conference on Robotics and Automation},\n  pages = {4075-4081},\n  year = {2013},\n  address = {Karlsruhe, Germany},\n  publisher = {&copy; ieee press},\n  url_Paper = {2013/RPK13.pdf},\n  keywords = {Games,Synthesis},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Rabin index of parity games.\n \n \n \n \n\n\n \n Huth, M.; Kuo, J. H.; and Piterman, N.\n\n\n \n\n\n\n In 4th International Symposium on Games, Automata, Logics and Formal Verification, volume 119, of EPTCS, pages 35-49, Borca di Cadore, Dolomites, Italy, August 2013. \n \n\n\n\n
\n\n\n\n \n \n \"The paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@inproceedings{HKP13b,\n  author    = {M. Huth and J. H. Kuo and N. Piterman},\n  title     = {The Rabin index of parity games},\n  year      = {2013},\n  pages     = {35-49},\n  booktitle     = {4th International Symposium on Games, Automata,\n               Logics and Formal Verification},\n  address = {Borca di Cadore, Dolomites, Italy},\n  month = {August},\n  series    = {EPTCS},\n  url_Paper = {2013/HKP13b.pdf},\n  volume    = {119},\n  keywords = {Games},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Fatal Attractors in Parity Games.\n \n \n \n \n\n\n \n Huth, M.; Kuo, J.; and Piterman, N.\n\n\n \n\n\n\n In 16th International Conference on Foundations of Software Science and Computation Structures, volume 7794, of Lecture Notes in Computer Science, pages 34-49, Rome, Italy, 2013. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Fatal paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{HKP13,\n  author = \t {M. Huth and J.H. Kuo and N. Piterman},\n  title = \t {Fatal Attractors in Parity Games},\n  booktitle = {16th International Conference on Foundations of Software Science and Computation Structures},\n  pages = \t {34-49},\n  year = \t {2013},\n  volume = \t {7794},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {Rome, Italy},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2013/HKP13.pdf},\n  keywords = {Games},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesising Non-Anomalous Event-Based Controllers for Liveness Goals.\n \n \n \n \n\n\n \n D'Ippolito, N.; Braberman, V.; Piterman, N.; and Uchitel, S.\n\n\n \n\n\n\n Transactions on Software Engineering and Methodology, 22(1): 9. 2013.\n \n\n\n\n
\n\n\n\n \n \n \"Synthesising paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{DBPU13,\n  author = \t {N. D'Ippolito and V. Braberman and N. Piterman and S. Uchitel},\n  title        = {Synthesising Non-Anomalous Event-Based Controllers for Liveness Goals},\n  journal      = {Transactions on Software Engineering and Methodology},\n  year         = {2013},\n  publisher    = {ACM},\n  volume = \t {22},\n  number = \t {1},\n  pages = \t {9},\n  url_Paper = {2013/DBPU13.pdf},\n  keywords = {Synthesis,Model Driven Development},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n At the Interface of Biology and Computation.\n \n \n \n \n\n\n \n Taylor, A.; Benque, D.; Cockerton, C.; Cook, B.; Fisher, J.; Ishtiaq, S.; and Piterman, N.\n\n\n \n\n\n\n In ACM SIGCHI Conference on Human Factors in Computing Systems, pages 493-502, Paris, France, 2013. ACM\n \n\n\n\n
\n\n\n\n \n \n \"At paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{TBCCFIP13,\n  author = \t {A. Taylor and D. Benque and C. Cockerton and B. Cook and J. Fisher and S. Ishtiaq and N. Piterman},\n  title = \t {At the Interface of Biology and Computation},\n  booktitle = {ACM SIGCHI Conference on Human Factors in Computing Systems},\n  pages = \t {493-502},\n  year = \t {2013},\n  address = \t {Paris, France},\n  publisher = {ACM},\n  keywords = {Executable Biology},\n  url_Paper = {2013/TPIFCCBB13.pdf},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesis of Biological Models from Mutation Experiments.\n \n \n \n \n\n\n \n Koskal, A.; Pu, Y.; Srivastava, S.; Bodik, R.; Piterman, N.; and Fisher, J.\n\n\n \n\n\n\n In 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, volume 7794, pages 34-49, Rome, Italy, 2013. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Synthesis paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{KPSBPF13,\n  author = \t {A.S. Koskal and Y. Pu and S. Srivastava and R. Bodik and N. Piterman and J. Fisher},\n  title = \t {Synthesis of Biological Models from Mutation Experiments},\n  booktitle = {40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},\n  pages = \t {34-49},\n  year = \t {2013},\n  volume = \t {7794},\n  address = \t {Rome, Italy},\n  publisher = {ACM},\n  keywords = {Synthesis,Executable Biology},\n  url_Paper = {2013/KPSBPF13.pdf},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2012\n \n \n (8)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Cell-cycle regulation of NOTCH signaling during C. elegans vulval development.\n \n \n \n \n\n\n \n Nusser-Stein, S.; Beyer, A.; Rimann, I.; Adamczyk, M.; Piterman, N.; Hajnal, A.; and Fisher, J.\n\n\n \n\n\n\n Molecular Systems Biology, 8(618). 2012.\n \n\n\n\n
\n\n\n\n \n \n \"Cell-cycle link\n  \n \n \n \"Cell-cycle paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{NBRAPHF12,\n  author = {S. Nusser-Stein and A. Beyer and I. Rimann and M. Adamczyk and N. Piterman and A. Hajnal and J. Fisher},\n  title = {Cell-cycle regulation of NOTCH signaling during C. elegans vulval development},\n  journal = {Molecular Systems Biology},\n  year = {2012},\n  volume = {8},\n  number = {618},\n  keywords = {Biology,Executable Biology},\n  url_Link = {http://www.nature.com/msb/journal/v8/n1/full/msb201251.html},\n  url_Paper = {http://www.nature.com/msb/journal/v8/n1/pdf/msb201251.pdf},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n p-Automata: New Foundations for Discrete-Time Probabilistic Verification.\n \n \n \n \n\n\n \n Huth, M.; Piterman, N.; and Wagner, D.\n\n\n \n\n\n\n Performance Evaluation, 69(7-8): 356-378. 2012.\n \n\n\n\n
\n\n\n\n \n \n \"p-Automata: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@Article{HPW12,\n  author = {M. Huth and N. Piterman and D. Wagner},\n  title = {p-Automata: New Foundations for Discrete-Time Probabilistic Verification},\n  journal = {Performance Evaluation},\n  year = {2012},\n  volume = {69},\n  number = {7-8},\n  pages = {356-378},\n  keywords = {Games, Model Checking,Automata},\n  url_Paper = {2012/HPW12.pdf},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Modal Transition System Control Problem.\n \n \n \n \n\n\n \n D'Ippolito, N.; Braberman, V.; Piterman, N.; and Uchitel, S.\n\n\n \n\n\n\n In 19th International Symposium on Formal Methods, volume 7436, of Lecture Notes in Computer Science, pages 155-170, Paris, France, 2012. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"The paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{DBPU12,\n  author = \t {N. D'Ippolito and V. Braberman and N. Piterman and S. Uchitel},\n  title = \t {The Modal Transition System Control Problem},\n  booktitle = {19th International Symposium on Formal Methods},\n  pages = \t {155-170},\n  year = \t {2012},\n  volume = \t {7436},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {Paris, France},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2012/DBPU12.pdf},\n  keywords = {Synthesis,Model Driven Development,Games},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n BMA: Visual Tool for Modelling and Analyzing Biological Networks.\n \n \n \n \n\n\n \n Benque, D.; Bourton, S.; Cockerton, C.; Cook, B.; Fisher, J.; Ishtiaq, S.; Piterman, N.; Taylor, A.; and Vardi, M.\n\n\n \n\n\n\n In The 24th Conference on Computer Aided Verification, volume 7148, of Lecture Notes in Computer Science, pages 283-298, 2012. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"BMA: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@inproceedings{BBCCFIPTV12,\n  author = {D. Benque and S. Bourton and C. Cockerton and B. Cook and J. Fisher and S. Ishtiaq and N. Piterman and A. Taylor and M.Y. Vardi},\n  title = \t {{BMA}: Visual Tool for Modelling and Analyzing Biological Networks},\n  booktitle = {The 24th Conference on Computer Aided Verification},\n  series =    {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  pages = \t {283-298},\n  year = \t {2012},\n  volume = \t {7148},\n  url_Paper = {2012/BBCCFIPTV12.pdf},\n  keywords = {Executable Biology},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesis of Reactive(1) Designs.\n \n \n \n \n\n\n \n Bloem, R.; Jobstmann, B.; Piterman, N.; Pnueli, A.; and Sa'ar, Y.\n\n\n \n\n\n\n Journal of Computer and System Sciences, Special Issue in Memory of Amir Pneuli, 78(3): 911-938. May 2012.\n Full version of VMCAI06, DATE07, and COCV07 papers. See also the tools jTLV (obsolete) and slugs\n\n\n\n
\n\n\n\n \n \n \"Synthesis paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{BJPPS12,\n  author = \t {R. Bloem and B. Jobstmann and N. Piterman and A. Pnueli and Y. Sa'ar}, \n  title = \t {Synthesis of Reactive(1) Designs},\n  journal = \t {Journal of Computer and System Sciences, Special Issue in Memory of Amir Pneuli},\n  year = \t {2012},\n  volume = \t {78},\n  number = \t {3},\n  pages = \t {911-938},\n  month = \t {May},\n  url_Paper = {2012/BJPPS12.pdf},\n  note = \t {Full version of {VMCAI06}, {DATE07}, and {COCV07} papers. See also the tools <a href="http://www.wisdom.weizmann.ac.il/~saar/synthesis/">jTLV (obsolete)</a> and <a href="https://github.com/VerifiableRobotics/slugs">slugs</a>},\n  keywords =     {Synthesis,Games},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Predictive Modelling of Stem Cell Differentiation and Apoptosis in C. elegans.\n \n \n \n \n\n\n \n Beyer, A.; Eberhard, R.; Piterman, N.; Hengartner, M.; Hajnal, A.; and Fisher, J.\n\n\n \n\n\n\n In The Ninth International Conference on Information Processing in Cells and Tissues, volume 7148, of Lecture Notes in Computer Science, pages 283-298, 2012. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Predictive paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{BEPHHF12b,\n   author = {A. Beyer and R. Eberhard and N. Piterman and M.O. Hengartner and A. Hajnal and J. Fisher},\n  title = \t {Predictive Modelling \tof Stem Cell Differentiation and Apoptosis in C. elegans},\n  booktitle = {The Ninth International Conference on Information Processing in Cells and Tissues},\n  publisher = {&copy; Springer-Verlag},\n  series =    {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  pages = \t {283-298},\n  year = \t {2012},\n  volume = \t {7148},\n  url_Paper = {https://link.springer.com/chapter/10.1007%2F978-1-4419-7210-1_12},\n  keywords = {Biology,Executable Biology},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Dynamic Physical Model of Cell Migration, Differentiation and Apoptosis in Caenorhabditis Elegans.\n \n \n \n \n\n\n \n Beyer, A.; Eberhard, R.; Piterman, N.; Hengartner, M.; Hajnal, A.; and Fisher, J.\n\n\n \n\n\n\n Advances in Medicine and Experimental Biology, 736: 211-233. 2012.\n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{BEPHHF12a,\n   author = {A. Beyer and R. Eberhard and N. Piterman and M.O. Hengartner and A. Hajnal and J. Fisher},\n  title = \t {A Dynamic Physical Model of Cell Migration, Differentiation and Apoptosis in Caenorhabditis Elegans},\n  journal =   {Advances in Medicine and Experimental Biology},\n  year = {2012},\n  volume = {736},\n  pages =  {211-233},\n  url_Paper = {2012/BEPHHF12a.pdf},\n  keywords = {Biology,Executable Biology},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Effective Synthesis of Asynchronous Systems from GR(1) Specifications.\n \n \n \n \n\n\n \n Klein, U.; Piterman, N.; and Pnueli, A.\n\n\n \n\n\n\n In The Thirteenth International Conference on Verification, Model Checking, and Abstract Interpretation, volume 7148, of Lecture Notes in Computer Science, pages 283-298, 2012. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Effective paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{KPP12,\n  author = \t {U. Klein and N. Piterman and A. Pnueli},\n  title = \t {Effective Synthesis of Asynchronous Systems from GR(1) Specifications},\n  booktitle = {The Thirteenth International Conference on Verification, Model Checking, and Abstract Interpretation},\n  series =    {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  pages = \t {283-298},\n  year = \t {2012},\n  volume = \t {7148},\n  url_Paper = {2012/KPP12.pdf},\n    keywords = {Synthesis,Games},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2011\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Concurrent Small Progress Measures.\n \n \n \n \n\n\n \n Huth, M.; Kuo, J.; and Piterman, N.\n\n\n \n\n\n\n In Haifa Verification Conference, volume 7261, of Lecture Notes in Computer Science, pages 130-144, 2011. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Concurrent paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{HKP11,\n  author = \t {M. Huth and J.H. Kuo and N. Piterman},\n  title = \t {Concurrent Small Progress Measures},\n  booktitle = {Haifa Verification Conference},\n  series =    {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  pages = \t {130-144},\n  year = \t {2011},\n  volume = \t {7261},\n  url_Paper = {2011/HKP11.pdf},\n  keywords = {Games},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n p-Automata and Obligation Games.\n \n \n \n \n\n\n \n Piterman, N.\n\n\n \n\n\n\n In 18th International Symposium on Temporal Representation and Reasoning, pages 3-6, 2011. © ieee press\n \n\n\n\n
\n\n\n\n \n \n \"p-Automata paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{Pit11,\n  author = \t {N. Piterman},\n  title = \t {p-Automata and Obligation Games},\n  booktitle = {18th International Symposium on Temporal Representation and Reasoning},\n  pages = \t {3-6},\n  year = \t {2011},\n  url_Paper = {2011/Pit11.pdf},\n  publisher = {&copy; ieee press},\n    keywords = {Automata,Games},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Dynamic Reactive Modules.\n \n \n \n \n\n\n \n Fisher, J.; Henzinger, T.; Nickovic, D.; Singh, A.; Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In 22nd International Conference on Concurrency Theory, volume 6901, of Lecture Notes in Computer Science, pages 404-418, 2011. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Dynamic paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{FHNSPV11,\n  author = \t {J. Fisher and T.A. Henzinger and D. Nickovic and A.V. Singh and N. Piterman and M.Y. Vardi},\n  title = \t {Dynamic Reactive Modules},\n  booktitle = {22nd International Conference on Concurrency Theory},\n  pages = \t {404-418},\n  year = \t {2011},\n  volume = \t {6901},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2011/FHNSPV11.pdf},\n  keywords = {Executable Biology},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Only Way Is Up.\n \n \n \n \n\n\n \n Fisher, J.; Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In 17th International Symposium on Formal Methods, volume 6664, of Lecture Notes in Computer Science, pages 3-11, 2011. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"The paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{FPV11,\n   author = {J. Fisher and N. Piterman and M.Y. Vardi},\n   title = {The Only Way Is Up},\n   year = {2011},\n   booktitle = {17th International Symposium on Formal Methods},\n  pages = \t {3-11},\n  year = \t {2011},\n  volume = \t {6664},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2011/FPV11.pdf},\nkeywords = {Executable Biology}\n}\n      \n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesis of Live Behavior Models for Fallible Domains.\n \n \n \n \n\n\n \n D'Ippolito, N.; Braberman, V.; Piterman, N.; and Uchitel, S.\n\n\n \n\n\n\n In 33rd International Conference on Software Engineering, pages 211-220, 2011. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Synthesis paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{DBPU11,\n  author = \t {N. D'Ippolito and V. Braberman and N. Piterman and S. Uchitel},\n  title = \t {Synthesis of Live Behavior Models for Fallible Domains},\n  booktitle = {33rd International Conference on Software Engineering},\n  pages = \t {211-220},\n  year = \t {2011},\n  url_Paper = {2011/DBPU11.pdf},\n  publisher = {ACM},\n  keywords = {Synthesis,Model Driven Development},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Proving stabilization of biological systems.\n \n \n \n \n\n\n \n Cook, B.; Fisher, J.; Krepska, E.; and Piterman, N.\n\n\n \n\n\n\n In 12th International Conference on Verification, Model Checking, and Abstract Interpretation, volume 6538, of Lecture Notes in Computer Science, pages 134-149, 2011. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Proving paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{CFKP11,\n  author = \t {B. Cook and J. Fisher and E. Krepska and N. Piterman},\n  title = \t {Proving stabilization of biological systems},\n  booktitle = {12th International Conference on Verification, Model Checking, and Abstract Interpretation},\n  pages = \t {134-149},\n  year = \t {2011},\n  volume = \t {6538},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2011/CFKP11.pdf},\n  keywords = {Executable Biology,Model Checking},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Generalized Model Checking Revisited.\n \n \n \n \n\n\n \n Godefroid, P.; and Piterman, N.\n\n\n \n\n\n\n Software Tools for Technology Transfer, 13(6): 571-584. November 2011.\n \n\n\n\n
\n\n\n\n \n \n \"Generalized paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@Article{GP11,\n  author = \t {P. Godefroid and N. Piterman},\n  title = \t {Generalized Model Checking Revisited},\n  journal =   {Software Tools for Technology Transfer},\n  year = {2011},\n  volume = {13},\n  number = {6},\n  pages =  {571-584},\n  url_Paper = {2011/GP11.pdf},\n  month =  {November},\n  keywords = {Model Checking},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2010\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Synthesis of Live Behavior Models.\n \n \n \n \n\n\n \n D'Ippolito, N.; Braberman, V.; Piterman, N.; and Uchitel, S.\n\n\n \n\n\n\n In 18th International Symposium on Foundations of Software Engineering, pages 77-86, 2010. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Synthesis paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{DBPU10,\n  author = \t {N. D'Ippolito and V. Braberman and N. Piterman and S. Uchitel},\n  title = \t {Synthesis of Live Behavior Models},\n  booktitle = {18th International Symposium on Foundations of Software Engineering},\n  pages = \t {77-86},\n  year = \t {2010},\n  publisher = {ACM},\n  url_Paper = \t {2010/DBPU10.pdf},\n  keywords = {Synthesis,Model Driven Development},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Automata Theoretic Approach to Infinite-State Systems.\n \n \n \n \n\n\n \n Kupferman, O.; Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In Time for Verification: Essays in Memory of Amir Pnueli, volume 6200, of Lecture Notes in Computer Science, pages 202-259. © Springer-Verlag, 2010.\n \n\n\n\n
\n\n\n\n \n \n \"Automata paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InCollection{KPV10,\n  author = \t {O. Kupferman and N. Piterman and M.Y. Vardi},\n  title = \t {Automata Theoretic Approach to Infinite-State Systems},\n  booktitle = \t {Time for Verification: Essays in Memory of Amir Pnueli},\n  pages = \t {202-259},\n  publisher = {&copy; Springer-Verlag},\n  year = \t {2010},\n  volume = \t {6200},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  url_Paper = \t {2010/KPV10.pdf},\n  keywords = {Model Checking,Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n p-Automata: New Foundations for Discrete-Time Probabilistic Verification.\n \n \n \n \n\n\n \n Huth, M.; Piterman, N.; and Wagner, D.\n\n\n \n\n\n\n In 7th International Conference on Quantitative Evaluation of SysTems, pages 161-170, 2010. © ieee press\n \n\n\n\n
\n\n\n\n \n \n \"p-Automata: paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{HPW10,\n  author =       {M. Huth and N. Piterman and D. Wagner},\n  title = \t {p-Automata: New Foundations for Discrete-Time Probabilistic Verification},\n  booktitle = {7th International Conference on Quantitative Evaluation of SysTems},\n  pages = \t {161-170},\n  year = \t {2010},\n  publisher = {&copy; ieee press},\n  url_Paper = \t {2010/HPW10.pdf},\n  keywords = {Automata,Model Checking},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n From MTL to Deterministic Timed Automata.\n \n \n \n \n\n\n \n Nickovic, D.; and Piterman, N.\n\n\n \n\n\n\n In 8th International Conference on Formal Modelling and Analysis of Timed Systems, volume 6246, of Lecture Notes in Computer Science, pages 152-167, 2010. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"From paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{NP10,\n  author = \t {D. Nickovic and N. Piterman},\n  title = \t {From MTL to Deterministic Timed Automata},\n  booktitle = {8th International Conference on Formal Modelling and Analysis of Timed Systems},\n  pages = \t {152-167},\n  year = \t {2010},\n  volume = \t {6246},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  url_Paper = {2010/NP10.pdf},\n  publisher = {&copy; Springer-Verlag},\n  keywords = {Temporal Logic,Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Strategy Logic.\n \n \n \n \n\n\n \n Chatterjee, K.; Henzinger, T.; and Piterman, N.\n\n\n \n\n\n\n Information and Computation, 208(6): 677-693. June 2010.\n \n\n\n\n
\n\n\n\n \n \n \"Strategy paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{CHP10,\n  author = \t {K. Chatterjee and T.A. Henzinger and N. Piterman},\n  title = \t {Strategy Logic},\n  journal =   {Information and Computation},\n  year = {2010},\n  volume = {208},\n  number = {6},\n  pages =  {677-693},\n  url_Paper = {2010/CHP10.pdf},\n  month =  {June},\n  keywords = {Synthesis,Games},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n PCTL Model Checking of Markov Chains: Truth and Falsity as Winning Strategies in Games.\n \n \n \n \n\n\n \n Fecher, H.; Huth, M.; Piterman, N.; and Wagner, D.\n\n\n \n\n\n\n Performance Evaluation, 67(9): 858-872. September 2010.\n \n\n\n\n
\n\n\n\n \n \n \"PCTL paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{FHPW10,\n  author = \t {H. Fecher and M. Huth and N. Piterman and D. Wagner},\n  title = {PCTL Model Checking of Markov Chains: Truth and Falsity as \nWinning Strategies in Games},\n  journal =   {Performance Evaluation},\n  year = {2010},\n  volume = {67},\n  number = {9},\n  pages =  {858-872},\n  url_Paper = {2010/FHPW10.pdf},\n  month =  {September},\n  keywords = {Model Checking,Games},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The Executable Pathway to Biological Networks.\n \n \n \n \n\n\n \n Fisher, J.; and Piterman, N.\n\n\n \n\n\n\n Briefings in Functional Genomics and Proteomics, 9(1): 79-92. January 2010.\n \n\n\n\n
\n\n\n\n \n \n \"The paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@Article{FP10,\n   author = {J. Fisher and N. Piterman},\n   title = {The Executable Pathway to Biological Networks},\n   year = {2010},\n   journal = {Briefings in Functional Genomics and Proteomics},\n   volume = {9},\n   number = {1},\n   pages = {79-92},\n   month = {January},\n   url_Paper = {2010/FP10.pdf},\n  keywords = {Executable Biology},\n}\n      \n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2009\n \n \n (6)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Computational Modeling of the EGFR Network Elucidates Control Mechanisms Regulating Signal Dynamics.\n \n \n \n \n\n\n \n Wang, D.; Cardelli, L.; Phillips, A.; Piterman, N.; and Fisher, J.\n\n\n \n\n\n\n BMC Systems Biology, 3(1): 118. December 2009.\n \n\n\n\n
\n\n\n\n \n \n \"Computational link\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{WCPPF09,\n   author = {D.Y.Q. Wang and L. Cardelli and A. Phillips and N. Piterman and J. Fisher},\n   title = {Computational Modeling of the EGFR Network Elucidates Control Mechanisms Regulating Signal Dynamics},\n   year = {2009},\n   journal = {BMC Systems Biology},\n   volume = {3},\n   number = {1},\n   pages = {118},\n   month = {December},\n   url_Link = {http://www.biomedcentral.com/1752-0509/3/118},  \n  keywords = {Biology,Executable Biology},\n}\n      \n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Workbench for PreProcessor Design and Evaulation: toward Benchmarks for Parity Games.\n \n \n \n \n\n\n \n Huth, M.; Piterman, N.; and Wang, H.\n\n\n \n\n\n\n 2009.\n \n\n\n\n
\n\n\n\n \n \n \"A paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@Workshop{HPW09a,\n  author = \t {M. Huth and N. Piterman and H. Wang},\n  title = \t {A Workbench for PreProcessor Design and Evaulation: toward Benchmarks for Parity Games},\n  booktitle = {9th International Workshop on Automated Verification of Critical Systems},\n  year = \t {2009},\n  volume = \t {23},\n  series = \t {Electronic Communications of the EASST},\n  publisher = {EASST},\n  url_Paper = {2009/HPW09b.pdf},\n  keywords = {Games},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Three-Valued Abstractions of Markov Chains: Completeness for a Sizeable Fragment of PCTL.\n \n \n \n \n\n\n \n Huth, M.; Piterman, N.; and Wagner, D.\n\n\n \n\n\n\n In 17th International Symposium on Fundamentals of Computation Theory, volume 5699, of Lecture Notes in Computer Science, pages 205-216, 2009. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Three-Valued paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{HPW09,\n  author = \t {M. Huth and N. Piterman and D. Wagner},\n  title = \t {Three-Valued Abstractions of Markov Chains: Completeness for a Sizeable Fragment of PCTL},\n  booktitle = {17th International Symposium on Fundamentals of Computation Theory},\n  pages = \t {205-216},\n  year = \t {2009},\n  volume = \t {5699},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2009/HPW09.pdf},\n  keywords = {Model Checking},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n From Liveness to Promptness.\n \n \n \n \n\n\n \n Kupferman, O.; Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n Formal Methods in System Design, 34(2): 83-103. 2009.\n \n\n\n\n
\n\n\n\n \n \n \"From paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{KPV09,\n  author =    {O. Kupferman and N. Piterman and M.Y. Vardi},\n  title =     {From Liveness to Promptness},\n  journal =   {Formal Methods in System Design},\n  volume = {34},\n  number = {2},\n  year = {2009},\n  pages =  {83-103},\n  url_Paper = {2009/KPV09.pdf},\n  keywords = {Model Checking,Temporal Logic},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Lower Bounds on Witnesses for Nonemptiness of Universal co-Buchi Automata.\n \n \n \n \n\n\n \n Kupferman, O.; and Piterman, N.\n\n\n \n\n\n\n In 12th International Conference on Foundations of Software Science and Computation Structures, volume 5504, of Lecture Notes in Computer Science, pages 182-196, 2009. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Lower paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{KP09,\n  author = \t {O. Kupferman and N. Piterman},\n  title = \t {Lower Bounds on Witnesses for Nonemptiness of Universal co-Buchi Automata},\n  booktitle = {12th International Conference on Foundations of \nSoftware Science and Computation Structures},\n  pages = \t {182-196},\n  year = \t {2009},\n  volume = \t {5504},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2009/KP09.pdf},\n  keywords = {Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n LTL Generalized Model Checking Revisited.\n \n \n \n \n\n\n \n Godefroid, P.; and Piterman, N.\n\n\n \n\n\n\n In 10th International Conference on Verification, Model Checking, and Abstract Interpretation, volume 5403, of Lecture Notes in Computer Science, pages 89-103, 2009. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"LTL paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{GP09,\n  author = \t {P. Godefroid and N. Piterman},\n  title = \t {LTL Generalized Model Checking Revisited},\n  booktitle = {10th International Conference on Verification, Model \nChecking, and Abstract Interpretation},\n  pages = \t {89-103},\n  year = \t {2009},\n  volume = \t {5403},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2009/GP09.pdf},\n  keywords = {Model Checking},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2008\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Hintikka Games for PCTL on Labeled Markov Chains.\n \n \n \n \n\n\n \n Fecher, H.; Huth, M.; Piterman, N.; and Wagner, D.\n\n\n \n\n\n\n In 5th International Conference on the Quantitative Evaluaiton of Systems, pages 169-178, 2008. © ieee press\n \n\n\n\n
\n\n\n\n \n \n \"Hintikka paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{FHPW08,\n  author = \t {H. Fecher and M. Huth and N. Piterman and D. Wagner},\n  title = \t {Hintikka Games for PCTL on Labeled Markov Chains},\n  booktitle = {5th International Conference on the Quantitative \nEvaluaiton of Systems},\n  pages = \t {169-178},\n  year = \t {2008},\n  publisher = {&copy; ieee press},\n  url_Paper = {2008/FHPW08.pdf},\n  keywords = {Model Checking,Games},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Bounded Asynchrony for Modeling Cell-Cell Interactions.\n \n \n \n \n\n\n \n Fisher, J.; Henzinger, T.; Mateescu, M.; and Piterman, N.\n\n\n \n\n\n\n In 1st Workshop on Formal Methods in Systems Biology, volume 5054, of Lecture Notes in Computer Science, pages 17-32, 2008. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Bounded paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{FHMP08,\n  author = \t {J. Fisher and T.A. Henzinger and M. Mateescu and N. Piterman},\n  title = \t {Bounded Asynchrony for Modeling Cell-Cell Interactions},\n  booktitle = {1st Workshop on Formal Methods in Systems Biology},\n  pages = \t {17-32},\n  year = \t {2008},\n  volume = \t {5054},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2008/FHMP08.pdf},\n  keywords = {Executable Biology,Modelling},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2007\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata.\n \n \n \n \n\n\n \n Piterman, N.\n\n\n \n\n\n\n Logical Methods in Computer Science, 3(3): 5. 2007.\n see a tighter analysis by Wanwei Liu and by Sven Schewe\n\n\n\n
\n\n\n\n \n \n \"From paper\n  \n \n \n \"From link\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@Article{Pit07,\n  author = \t {N. Piterman},\n  title = \t {From Nondeterministic Buchi and Streett Automata to \nDeterministic Parity Automata},\n  journal = \t {Logical Methods in Computer Science},\n  year = \t {2007},\n  volume = \t {3},\n  number = \t {3},\n  pages = \t {5},\n  url_Paper = {https://lmcs.episciences.org/1199/pdf},\n  url_Link = {https://lmcs.episciences.org/1199},\n  note = {see a tighter analysis</a> by <a href=http://dx.doi.org/10.1016/j.ipl.2009.04.022>Wanwei Liu</a> and by <a href=http://dx.doi.org/10.1007/978-3-642-00596-1_13>Sven Schewe</a>},\n  keywords = {Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Strategy Logic.\n \n \n \n \n\n\n \n Chatterjee, K.; Henzinger, T.; and Piterman, N.\n\n\n \n\n\n\n In 18th International Conference on Concurrency Theory, volume 4703, of Lecture Notes in Computer Science, pages 59-73, 2007. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Strategy paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{CHP07b,\n  author = \t {K. Chatterjee and T.A. Henzinger and N. Piterman},\n  title = \t {Strategy Logic},\n  booktitle = {18th International Conference on Concurrency \nTheory},\n  pages = \t {59-73},\n  year = \t {2007},\n  volume = \t {4703},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2007/CHP07a.pdf},\n  keywords = {Games},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n From Liveness to Promptness.\n \n \n \n \n\n\n \n Kupferman, O.; Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In 18th Conference on Computer Aided Verification, volume 4590, of Lecture Notes in Computer Science, pages 411-424, 2007. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"From paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{KPV07,\n  author = \t {O. Kupferman and N. Piterman and M.Y. Vardi},\n  title = \t {From Liveness to Promptness},\n  booktitle = {18th Conference on Computer Aided Verification},\n  pages = \t {411-424},\n  year = \t {2007},\n  volume = \t {4590},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2007/KPV07.pdf},\n  keywords = {Model Checking,Temporal Logic},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Predictive Modeling of Signaling Crosstalk during C. elegans Vulval Development.\n \n \n \n \n\n\n \n Fisher, J.; Piterman, N.; Hajnal, A.; and Henzinger, T.\n\n\n \n\n\n\n PLoS Computational Biology, 3(5): e92. 2007.\n \n\n\n\n
\n\n\n\n \n \n \"Predictive link\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{FPHH07,\n  author = \t {J. Fisher and N. Piterman and A. Hajnal and T.A. Henzinger},\n  title = \t {Predictive Modeling of Signaling Crosstalk during <i>C. \nelegans</i> Vulval Development},\n  journal = \t {PLoS Computational Biology},\n  year = \t {2007},\n  volume = \t {3},\n  number = \t {5},\n  pages = \t {e92},\n  url_Link = {http://compbiol.plosjournals.org/perlserv/?request=get-document&doi=10.1371/journal.pcbi.0030092},\n  keywords = {Biology,Executable Biology},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Specify, Compile, Run: Hardware from PSL.\n \n \n \n \n\n\n \n Bloem, R.; Galler, S.; Jobstmann, B.; Piterman, N.; Pnueli, A.; and Weiglhofer, M.\n\n\n \n\n\n\n In 6th International Workshop on Compiler Optimization Meets Compiler Verification, volume 190, of Electronic Notes in Theoretical Computer Science, pages 3-16, 2007. \n \n\n\n\n
\n\n\n\n \n \n \"Specify, paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{BGJPPW07b,\n  author = \t {R. Bloem and S. Galler and B. Jobstmann and N. Piterman and A. Pnueli and M. Weiglhofer},\n  title = \t {Specify, Compile, Run: Hardware from PSL},\n  booktitle = {6th International Workshop on Compiler Optimization Meets \nCompiler Verification},\n  pages = \t {3-16},\n  year = \t {2007},\n  volume = \t {190},\n  number =       {4},  \n  series = \t {Electronic Notes in Theoretical Computer Science},\n  url_Paper = {2007/BGJPPW07a.pdf},\n  keywords = {Synthesis},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Automatic Hardware Synthesis from Specifications: A Case Study.\n \n \n \n \n\n\n \n Bloem, R.; Galler, S.; Jobstmann, B.; Piterman, N.; Pnueli, A.; and Weiglhofer, M.\n\n\n \n\n\n\n In Design Automation and Test in Europe, pages 1188-1193, 2007. ACM\n \n\n\n\n
\n\n\n\n \n \n \"Automatic paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{BGJPPW07a,\n  author = \t {R. Bloem and S. Galler and B. Jobstmann and N. Piterman and A. Pnueli and M. Weiglhofer},\n  title = \t {Automatic Hardware Synthesis from Specifications: A Case Study},\n  booktitle = {Design Automation and Test in Europe},\n  pages = \t {1188-1193},\n  year = \t {2007},\n  publisher = {ACM},\n  url_Paper = {2007/BGJPPW07.pdf},\n  keywords = {Synthesis},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Generalized Parity Games.\n \n \n \n \n\n\n \n Chatterjee, K.; Henzinger, T.; and Piterman, N.\n\n\n \n\n\n\n In 10th International Conference on Foundations of Software Science and Computation Structures, volume 4423, of Lecture Notes in Computer Science, pages 153-167, 2007. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Generalized paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{CHP07a,\n  author = \t {K. Chatterjee and T.A. Henzinger and N. Piterman},\n  title = \t {Generalized Parity Games},\n  booktitle = {10th International Conference on Foundations of Software Science and Computation Structures},\n  pages = \t {153-167},\n  year = \t {2007},\n  volume = \t {4423},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2007/CHP07.pdf},\n  keywords = {Games},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2006\n \n \n (9)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Solving Games without Determinization.\n \n \n \n \n\n\n \n Henzinger, T.; and Piterman, N.\n\n\n \n\n\n\n In 15th Conference on Computer Science Logic, volume 4207, of Lecture Notes in Computer Science, pages 394-409, 2006. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Solving paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{HP06,\n  author = \t {T.A. Henzinger and N. Piterman},\n  title = \t {Solving Games without Determinization},\n  booktitle = {15th Conference on Computer Science Logic},\n  pages = \t {394-409},\n  year = \t 2006,\n  volume = \t {4207},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2006/HP06.pdf},\n  keywords = {Games,Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Algorithms for Buchi Games.\n \n \n \n \n\n\n \n Chatterjee, K.; Henzinger, T.; and Piterman, N.\n\n\n \n\n\n\n In 3rd Workshop on Games in Design and Verification, 2006. \n \n\n\n\n
\n\n\n\n \n \n \"Algorithms paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{CHP06,\n  author = \t {K. Chatterjee and T.A. Henzinger and N. Piterman},\n  title = \t {Algorithms for Buchi Games},\n  booktitle = {3rd  Workshop on Games in Design and Verification},\n  OPTpages = \t {},\n  year = \t 2006,\n  OPTvolume = \t {},\n  OPTseries = \t {},\n  OPTpublisher = {},\n  url_Paper = {2006/CHP06.pdf},\n  keywords = {Games},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Inferring Network Invariants Automatically.\n \n \n \n \n\n\n \n Grinchtein, O.; Leucker, M.; and Piterman, N.\n\n\n \n\n\n\n In 3rd International Joint Conference on Automated Reasoning, volume 4130, of Lecture Notes in Computer Science, pages 483-497, 2006. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Inferring paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{GLP06,\n  author = \t {O. Grinchtein and M. Leucker and N. Piterman},\n  title = \t {Inferring Network Invariants Automatically},\n  booktitle = {3rd International Joint Conference on Automated \nReasoning},\n  pages = \t {483-497},\n  year = \t 2006,\n  volume = \t {4130},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2006/GLP06.pdf},\n  keywords = {Model Checking},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Safraless Compositional Synthesis.\n \n \n \n \n\n\n \n Kupferman, O.; Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In 18th Conference on Computer Aided Verification, volume 4144, of Lecture Notes in Computer Science, pages 31-44, 2006. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Safraless paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{KPV06,\n  author = \t {O. Kupferman and N. Piterman and M.Y. Vardi},\n  title = \t {Safraless Compositional Synthesis},\n  booktitle = {18th Conference on Computer Aided Verification},\n  pages = \t {31-44},\n  year = \t 2006,\n  volume = \t {4144},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2006/KPV06.pdf},\n  keywords = {Synthesis,Automata,Games},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Minimizing Generalized Buchi Automata.\n \n \n \n \n\n\n \n Juvekar, S.; and Piterman, N.\n\n\n \n\n\n\n In 18th Conference on Computer Aided Verification, volume 4144, of Lecture Notes in Computer Science, pages 45-58, 2006. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Minimizing paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{JP06,\n  author = \t {S. Juvekar and N. Piterman},\n  title = \t {Minimizing Generalized Buchi Automata},\n  booktitle = {18th Conference on Computer Aided Verification},\n  pages = \t {45-58},\n  year = \t 2006,\n  volume = \t {4144},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2006/JP06.pdf},\n  keywords = {Automata,Games},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata.\n \n \n \n \n\n\n \n Piterman, N.\n\n\n \n\n\n\n In 21st Symposium on Logic in Computer Science, pages 255-264, 2006. © ieee press\n see a tighter analysis by Wanwei Liu and by Sven Schewe\n\n\n\n
\n\n\n\n \n \n \"From paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{Pit06,\n  author = \t {N. Piterman},\n  title = \t {From Nondeterministic {B}uchi and {S}treett Automata to Deterministic Parity Automata},\n  booktitle = {21st Symposium on Logic in Computer Science},\n  pages = \t {255-264},\n  year = \t {2006},\n  publisher = {&copy; ieee press},\n  url_Paper = {2006/Pit06.pdf},\n  note = {see a tighter analysis</a> by <a href=http://dx.doi.org/10.1016/j.ipl.2009.04.022>Wanwei Liu</a> and by <a href=http://dx.doi.org/10.1007/978-3-642-00596-1_13>Sven Schewe</a>},\n  keywords = {Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Faster Solutions of Rabin and Streett Games.\n \n \n \n \n\n\n \n Piterman, N.; and Pnueli, A.\n\n\n \n\n\n\n In 21st Symposium on Logic in Computer Science, pages 275-284, 2006. © ieee press\n \n\n\n\n
\n\n\n\n \n \n \"Faster paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{PP06,\n  author = \t {N. Piterman and A. Pnueli},\n  title = \t {Faster Solutions of Rabin and Streett Games},\n  booktitle = {21st Symposium on Logic in Computer Science},\n  pages = \t {275-284},\n  year = \t {2006},\n  publisher = {&copy; ieee press},\n  url_Paper = {2006/PP06.pdf},\n  keywords = {Games},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Liveness with Invisible Ranking.\n \n \n \n \n\n\n \n Fang, Y.; Piterman, N.; Pnueli, A.; and Zuck, L.\n\n\n \n\n\n\n Software Tools for Technology Transfer, 8(3): 261-279. 2006.\n \n\n\n\n
\n\n\n\n \n \n \"Liveness paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@Article{FPPZ06,\n  author = \t {Y. Fang and N. Piterman and A. Pnueli and L. Zuck},\n  title = \t {Liveness with Invisible Ranking},\n  journal = \t {Software Tools for Technology Transfer},\n  year = \t {2006},\n  volume = \t {8},\n  number = \t {3},\n  pages = \t {261-279},\n  url_Paper = {2006/FPPZ06.pdf},\n  keywords = {Model Checking},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Synthesis of Reactive(1) Designs.\n \n \n \n \n\n\n \n Piterman, N.; Pnueli, A.; and Sa'ar, Y.\n\n\n \n\n\n\n In 7th International Conference on Verification, Model Checking and Abstract Interpretation, volume 3855, of Lecture Notes in Computer Science, pages 364-380, January 2006. © Springer-Verlag\n See also the tools jTLV (obsolete) and slugs\n\n\n\n
\n\n\n\n \n \n \"Synthesis paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{PPS06,\n  author = \t {N. Piterman and A. Pnueli and Y. Sa'ar},\n  title = \t {Synthesis of Reactive(1) Designs},\n  booktitle = {7th International Conference on Verification, Model Checking and Abstract Interpretation},\n  pages = \t {364-380},\n  year = \t {2006},\n  volume = \t {3855},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  month = \t {January},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2006/PPS06.pdf},\n  note = {See also the tools <a href="http://www.wisdom.weizmann.ac.il/~saar/synthesis/">jTLV (obsolete)</a> and <a href="https://github.com/VerifiableRobotics/slugs">slugs</a>},\n  keywords = {Synthesis,Games},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2005\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Bridging the Gap Between Fair Simulation and Trace Inclusion.\n \n \n \n \n\n\n \n Kesten, Y.; Piterman, N.; and Pnueli, A.\n\n\n \n\n\n\n Information and Computation, 200(1): 35-61. July 2005.\n \n\n\n\n
\n\n\n\n \n \n \"Bridging paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{KPP05,\n  author =      {Y. Kesten and N. Piterman and A. Pnueli},\n  title =       {Bridging the Gap Between Fair Simulation and Trace Inclusion},\n  journal =     {Information and Computation},\n  year =        {2005},\n  volume =   {200},\n  number =   {1},\n  pages =    {35-61},\n  month =    {July},\n  url_Paper =      {2005/KPP05.pdf},\n  keywords = {Model Checking,Games},\n}  \n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Computational Insights into C. elegans Vulval Development.\n \n \n \n \n\n\n \n Fisher, J.; Piterman, N.; Hubbard, E.; Stern, M.; and Harel, D.\n\n\n \n\n\n\n Proceedings of the National Academy of Sciences, 102(6): 1951-1956. February 2005.\n \n\n\n\n
\n\n\n\n \n \n \"Computational paper\n  \n \n \n \"Computational link\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@Article{FPHSH05,\n  author = {J. Fisher and N. Piterman and E.J.A. Hubbard and M.J. Stern and D. Harel},\n  title = {Computational Insights into C. elegans Vulval Development},\n  journal = \t {Proceedings of the National Academy of Sciences},\n  year = \t {2005},\n  volume = \t {102},\n  number = \t {6},\n  pages = \t {1951-1956},\n  month = \t {February},\n  url_Paper =       {http://www.pnas.org/cgi/reprint/102/6/1951.pdf},\n  url_Link = \t {http://www.pnas.org/cgi/content/abstract/102/6/1951},\n  keywords = {Biology,Executable Biology},\n}\n\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2004\n \n \n (6)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Verification of Infinite-State Systems.\n \n \n \n \n\n\n \n Piterman, N.\n\n\n \n\n\n\n Ph.D. Thesis, The Weizmann Institute of Science, 2004.\n \n\n\n\n
\n\n\n\n \n \n \"Verification paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@PhdThesis{Pit04,\n   author = {N. Piterman},\n   title = {Verification of Infinite-State Systems},\n   school = {The Weizmann Institute of Science},\n   year = {2004},\n   url_Paper = {2004/phdthesis.pdf},\n  keywords = {Model Checking,Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n SAT-based Induction for Temporal Safety Properties.\n \n \n \n \n\n\n \n Armoni, R.; Fix, L.; Fraer, R.; Huddleston, S.; Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In 2nd International Workshop on Bounded Model Checking, volume 119, of Electronic Notes in Theoretical Computer Science, pages 3-16, Boston, MA, USA, July 2004. Elsevier\n \n\n\n\n
\n\n\n\n \n \n \"SAT-based paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{AFFHPV04,\n  author = \t {R. Armoni and L. Fix and R. Fraer and S. Huddleston and N. Piterman and M.Y. Vardi},\n  title = \t {SAT-based Induction for Temporal Safety Properties},\n  booktitle = {2nd International Workshop on Bounded Model Checking},\n  pages = \t {3-16},\n  year = \t {2004},\n  volume = \t {119},\n  number = \t {2},\n  series = \t {Electronic Notes in Theoretical Computer Science},\n  address = \t {Boston, MA, USA},\n  month = \t {July},\n  publisher = {Elsevier},\n  url_Paper = {2004/AFFHPV04.pdf},\n  keywords = {Model Checking},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Combining State-based and Scenario-based Approaches in Modeling Biological Systems.\n \n \n \n \n\n\n \n Fisher, J.; Harel, D.; Hubbard, E.; Piterman, N.; Stern, M.; and Swerdlin, N.\n\n\n \n\n\n\n In 2nd International Workshop on Computational Methods in Systems Biology, volume 3082, of Lecture Notes in Computer Science, pages 236-241, Paris, France, May 2004. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Combining paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{FHHPSS04,\n  author = \t {J. Fisher and D. Harel and E.J.A. Hubbard and N. Piterman and M.J. Stern and N. Swerdlin},\n  title = \t {Combining State-based and Scenario-based Approaches in Modeling Biological Systems},\n  booktitle = {2nd International Workshop on Computational Methods in Systems Biology},\n  pages = \t {236-241},\n  year = \t {2004},\n  volume = \t {3082},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {Paris, France},\n  month = \t {May},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = \t {2004/FHHPSS04.pdf},\n  keywords = {Executable Biology},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Global Model-Checking for Infinite-State Systems.\n \n \n \n \n\n\n \n Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In 16th International Conference on Computer Aided Verification, volume 3114, of Lecture Notes in Computer Science, pages 387-400, Boston, MA, USA, July 2004. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Global paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{PV04,\n  author = \t {N. Piterman and M.Y. Vardi},\n  title = \t {Global Model-Checking for Infinite-State Systems},\n  booktitle = {16th International Conference on Computer Aided Verification},\n  pages = \t {387-400},\n  year = \t {2004},\n  volume = \t {3114},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {Boston, MA, USA},\n  month = \t {July},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = \t {2004/PV04.pdf},\n  keywords = {Model Checking,Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Liveness with Incomprehensible Ranking.\n \n \n \n \n\n\n \n Fang, Y.; Piterman, N.; Pnueli, A.; and Zuck, L.\n\n\n \n\n\n\n In 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2988, of Lecture Notes in Computer Science, pages 482-496, Bercelona, Spain, March 2004. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Liveness paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{FPPZ04a,\n  author = \t {Y. Fang and N. Piterman and A. Pnueli and L. Zuck},\n  title = \t {Liveness with Incomprehensible Ranking},\n  booktitle = {10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},\n  pages = \t {482-496},\n  year = \t {2004},\n  volume = \t {2988},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {Bercelona, Spain},\n  month = \t {March},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = \t {2004/FPPZ04a.pdf},\n  keywords = {Model Checking},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Liveness with Invisible Ranking.\n \n \n \n \n\n\n \n Fang, Y.; Piterman, N.; Pnueli, A.; and Zuck, L.\n\n\n \n\n\n\n In 5th International Conference on Verification, Model Checking and Abstract Interpretation, volume 2937, of Lecture Notes in Computer Science, pages 223-238, Venice, Italy, January 2004. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Liveness paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{FPPZ04,\n  author = \t {Y. Fang and N. Piterman and A. Pnueli and L. Zuck},\n  title = \t {Liveness with Invisible Ranking},\n  booktitle = {5th International Conference on Verification, Model Checking and Abstract Interpretation},\n  pages = \t {223-238},\n  year = \t {2004},\n  volume = \t {2937},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {Venice, Italy},\n  month = \t {January},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = \t {2004/FPPZ04.pdf},\n  keywords = {Model Checking},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2003\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Fair Equivalence Relations.\n \n \n \n \n\n\n \n Kupferman, O.; Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In Verification - Theory and Practice, Festschrift celebrating Zohar Manna's 64th Birthday, volume 2772, of Lecture Notes in Computer Science, pages 702-732. © Springer-Verlag, 2003.\n \n\n\n\n
\n\n\n\n \n \n \"Fair paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InCollection{KPV03,\n  author = \t {O. Kupferman and N. Piterman and M.Y. Vardi},\n  title = \t {Fair Equivalence Relations},\n  booktitle = \t {Verification - Theory and Practice, Festschrift celebrating Zohar Manna's 64th Birthday},\n  pages = \t {702-732},\n  publisher = {&copy; Springer-Verlag},\n  year = \t {2003},\n  volume = \t {2772},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  url_Paper = \t {2003/KPV03.pdf},\n  keywords = {Model Checking},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Bridging the Gap Between Fair Simulation and Trace Inclusion.\n \n \n \n \n\n\n \n Kesten, Y.; Piterman, N.; and Pnueli, A.\n\n\n \n\n\n\n In 15th International Conference on Computer Aided Verification, volume 2725, of Lecture Notes in Computer Science, pages 381-393, Boulder, CO, USA, July 2003. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Bridging paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{KPP03,\n  author = \t {Y. Kesten and N. Piterman and A. Pnueli},\n  title = \t {Bridging the Gap Between Fair Simulation and Trace Inclusion},\n  booktitle = \t {15th International Conference on Computer Aided Verification},\n  pages = \t {381-393},\n  year = \t {2003},\n  volume = \t {2725},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {Boulder, CO, USA},\n  month = \t {July},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2003/KPP03.pdf},\n  keywords = {Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Enhanced Vacuity Detection in Linear Temporal Logic.\n \n \n \n \n\n\n \n Armoni, R.; Fix, L.; Flaisher, A.; Grumberg, O.; Piterman, N.; Tiemeyer, A.; and Vardi, M.\n\n\n \n\n\n\n In 15th International Conference on Computer Aided Verification, volume 2725, of Lecture Notes in Computer Science, pages 368-380, Boulder, CO, USA, July 2003. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Enhanced paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{AFFGPTV03,\n  author = \t {R. Armoni and L. Fix and A. Flaisher and O. Grumberg and N. Piterman and A. Tiemeyer and M.Y. Vardi},\n  title = \t {Enhanced Vacuity Detection in Linear Temporal Logic},\n  booktitle = \t {15th International Conference on Computer Aided Verification},\n  pages = \t {368-380},\n  year = \t {2003},\n  volume = \t {2725},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {Boulder, CO, USA},\n  month = \t {July},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2003/AFFGPTV03.pdf},\n  keywords = {Model Checking},\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems.\n \n \n \n \n\n\n \n Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In 18th IEEE Symposium on Logic in Computer Science, pages 381-390, Ottawa, Canada, June 2003. IEEE, © IEEE press\n \n\n\n\n
\n\n\n\n \n \n \"Micro-Macro paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{PV03a,\n  author = \t {N. Piterman and M.Y. Vardi},\n  title = \t {Micro-Macro Stack Systems:\nA New Frontier of Elementary Decidability for Sequential Systems},\n  booktitle = \t {18th IEEE Symposium on Logic in Computer Science},\n  pages = \t {381-390},\n  year = \t {2003},\n  address = \t {Ottawa, Canada},\n  month = \t {June},\n  organization = {IEEE},\n  publisher = {&copy; IEEE press},\n  url_Paper = {2003/PV03a.pdf},\n  keywords = {Model Checking,Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n From Bidirectionality to Alternation.\n \n \n \n \n\n\n \n Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n Theoretical Computer Science, 295(1-3): 295-321. February 2003.\n \n\n\n\n
\n\n\n\n \n \n \"From paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@Article{PV03,\n  author = \t {N. Piterman and M.Y. Vardi},\n  title = \t {From Bidirectionality to Alternation},\n  journal = \t {Theoretical Computer Science},\n  year = \t {2003},\n  volume = \t {295},\n  number = \t {1-3},\n  pages = \t {295-321},\n  month = \t {February},\n  url_Paper =  {2003/PV03.pdf},\n  keywords = {Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2002\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Pushdown Specifications.\n \n \n \n \n\n\n \n Kupferman, O.; Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In 9th International Conference on Logic for Programming Artificial Intelligence and Reasoning, volume 2514, of Lecture Notes in Computer Science, pages 262-277, Tbilisi, Georgia, October 2002. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Pushdown paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{KPV02a,\n  author = \t {O. Kupferman and N. Piterman and M.Y. Vardi},\n  title = \t {Pushdown Specifications},\n  booktitle = \t {9th International Conference on Logic for Programming Artificial Intelligence and Reasoning},\n  pages = \t {262-277},\n  year = \t {2002},\n  volume = \t {2514},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {Tbilisi, Georgia},\n  month = \t {October},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2002/KPV02a.pdf},\n  keywords = {Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Model Checking Linear Properties of Prefix-Recognizable Systems.\n \n \n \n \n\n\n \n Kupferman, O.; Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In 14th International Conference on Computer Aided Verification, volume 2404, of Lecture Notes in Computer Science, pages 371-385, Copenhagen, Denmark, July 2002. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Model paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{KPV02,\n  author = \t {O. Kupferman and N. Piterman and M.Y. Vardi},\n  title = \t {Model Checking Linear Properties of Prefix-Recognizable Systems},\n  booktitle = \t {14th International Conference on Computer Aided Verification},\n  pages = \t {371-385},\n  year = \t {2002},\n  volume = \t {2404},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {Copenhagen, Denmark},\n  month = \t {July},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2002/kpv02.pdf},\n  keywords = {Model Checking,Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2001\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n From Bidirectionality to Alternation.\n \n \n \n \n\n\n \n Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In 26th International Symposium on Mathematical Foundations of Computer Science, volume 2136, of Lecture Notes in Computer Science, pages 598-610, Marianske Lazne, Czech Republic, August 2001. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"From paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@InProceedings{PV01,\n  author = \t {N. Piterman and M.Y. Vardi},\n  title = \t {From Bidirectionality to Alternation},\n  booktitle = \t {26th International Symposium on Mathematical Foundations of Computer Science},\n  pages = \t {598-610},\n  year = \t {2001},\n  volume = \t {2136},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {Marianske Lazne, Czech Republic},\n  month = \t {August},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper = {2001/pv01.pdf},\n  keywords = {Automata},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Extended Temporal Logic Revisited.\n \n \n \n \n\n\n \n Kupferman, O.; Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In 12th International conference on Concurrency theory, volume 2154, of Lecture Notes in Computer Science, pages 519-535, Aalborg, Denmark, August 2001. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Extended paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@InProceedings{KPV01,\n  author = \t {O. Kupferman and N. Piterman and M.Y. Vardi},\n  title = \t {Extended Temporal Logic Revisited},\n  booktitle = \t {12th International conference on Concurrency theory},\n  pages = \t {519-535},\n  year = \t {2001},\n  volume = \t {2154},\n  series = \t {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n  address = \t {Aalborg, Denmark},\n  month = \t {August},\n  publisher = {&copy; Springer-Verlag},\n  url_Paper =   {2001/kpv01.pdf},\n  keywords = {Automata,Temporal Logic},\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2000\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Fair Equivalence Relations.\n \n \n \n \n\n\n \n Kupferman, O.; Piterman, N.; and Vardi, M.\n\n\n \n\n\n\n In 20th Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 1974, of Lecture Notes in Computer Science, pages 151-163, December 2000. © Springer-Verlag\n \n\n\n\n
\n\n\n\n \n \n \"Fair paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@inproceedings{KPV00,\n\tauthor\t    =   {O. Kupferman and N. Piterman and M.Y. Vardi},\n\ttitle       =   {Fair Equivalence Relations},\n\tbooktitle   =   {20th Conference on the Foundations of\n                  Software Technology and Theoretical Computer\n                  Science}, \n        series      =   {<A HREF=http://www.springer.de/comp/lncs/index.html>Lecture Notes in Computer Science</A>},\n        volume      =   1974,\n        pages       =  {151-163}, \n        month       =\t{December},\n        publisher   =   {&copy; Springer-Verlag},\n\tyear        =\t{2000},\n\turl_Paper = {2000/fsttcs00.pdf},\n  keywords = {Model Checking},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Extending temporal logic with Omega-automata.\n \n \n \n \n\n\n \n Piterman, N.\n\n\n \n\n\n\n Master's thesis, The Weizmann Institute of Science, 2000.\n \n\n\n\n
\n\n\n\n \n \n \"Extending paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n\n\n\n
\n
@mastersthesis{Pit00,\n        author      =   {N. Piterman},\n        title       =   {Extending temporal logic with Omega-automata},\n        school      =   {The Weizmann Institute of Science},\n        year        =   {2000},\n\turl_Paper = {2000/msc_thesis.pdf},\n  keywords = {Automata,Temporal Logic},\n}\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);