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=https%3A%2F%2Fwww.math.unipd.it%2F%7Ebresolin%2Fpapers%2Fbiblio-it.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=https%3A%2F%2Fwww.math.unipd.it%2F%7Ebresolin%2Fpapers%2Fbiblio-it.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=https%3A%2F%2Fwww.math.unipd.it%2F%7Ebresolin%2Fpapers%2Fbiblio-it.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 2019\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Decidability and complexity of the fragments of the modal logic of Allen's relations over the rationals.\n \n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Montanari, A.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n Information and Computation. 2019.\n \n\n\n\n
\n\n\n\n \n \n \"DecidabilityPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \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\n
\n
@article{ic2019,\n\tAbstract = {Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as first-class citizens. Their expressive power and computational behavior mainly depend on two parameters: the set of modalities they feature and the linear orders over which they are interpreted. In this paper, we consider all fragments of Halpern and Shoham's interval temporal logic HS with a decidable satisfiability problem over the rationals, and we provide a complete classification of them in terms of their expressiveness and computational complexity by solving the last few open problems.},\n\tAuthor = {D. Bresolin and D. {Della Monica} and A. Montanari and P. Sala and G. Sciavicco},\n\tDate-Added = {2019-04-02 15:44:10 +0000},\n\tDate-Modified = {2019-04-05 12:45:20 +0000},\n\tDoi = {10.1016/j.ic.2019.02.002},\n\tIssn = {0890-5401},\n\tJournal = {Information and Computation},\n\tKeywords = {Interval temporal logics, Satisfiability, Decidability, Computational complexity},\n\tTitle = {Decidability and complexity of the fragments of the modal logic of Allen's relations over the rationals},\n\tUrl = {http://www.sciencedirect.com/science/article/pii/S0890540119300173},\n\tYear = {2019},\n\tBdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S0890540119300173},\n\tBdsk-Url-2 = {10.1016/j.ic.2019.02.002}}\n\n
\n
\n\n\n
\n Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as first-class citizens. Their expressive power and computational behavior mainly depend on two parameters: the set of modalities they feature and the linear orders over which they are interpreted. In this paper, we consider all fragments of Halpern and Shoham's interval temporal logic HS with a decidable satisfiability problem over the rationals, and we provide a complete classification of them in terms of their expressiveness and computational complexity by solving the last few open problems.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Minimizing Deterministic Timed Finite State Machines.\n \n \n \n \n\n\n \n Bresolin, D.; Tvardovskii, A.; Yevtushenko, N.; Villa, T.; and Gromov, M.\n\n\n \n\n\n\n In 14th IFAC Workshop on Discrete Event Systems WODES 2018, volume 51, issue 7, of IFAC-PapersOnLine, pages 486 - 492, 2018. \n \n\n\n\n
\n\n\n\n \n \n \"MinimizingPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\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{wodes2018,\n\tAuthor = {Davide Bresolin and Aleksandr Tvardovskii and Nina Yevtushenko and Tiziano Villa and Maxim Gromov},\n\tBooktitle = {14th IFAC Workshop on Discrete Event Systems WODES 2018},\n\tDate-Added = {2018-10-19 12:53:10 +0000},\n\tDate-Modified = {2018-10-19 12:55:56 +0000},\n\tDoi = {10.1016/j.ifacol.2018.06.344},\n\tKeywords = {Timed Finite State Machines, Minimization, Real-time systems, Automata theory, Timed Automata},\n\tPages = {486 - 492},\n\tSeries = {IFAC-PapersOnLine},\n\tTitle = {Minimizing Deterministic Timed Finite State Machines},\n\tUrl = {http://www.sciencedirect.com/science/article/pii/S2405896318306748},\n\tVolume = {51, issue 7},\n\tYear = {2018},\n\tBdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S2405896318306748},\n\tBdsk-Url-2 = {10.1016/j.ifacol.2018.06.344}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Extracting Interval Temporal Logic Rules: A First Approach.\n \n \n \n \n\n\n \n Bresolin, D.; Cominato, E.; Gnani, S.; Muñoz-Velasco, E.; and Sciavicco, G.\n\n\n \n\n\n\n In 25th International Symposium on Temporal Representation and Reasoning, TIME 2018, volume 120, of LIPIcs, pages 7:1–7:15, 2018. \n \n\n\n\n
\n\n\n\n \n \n \"ExtractingPaper\n  \n \n\n \n \n doi\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
@inproceedings{time2018,\n\tAuthor = {Davide Bresolin and Enrico Cominato and Simone Gnani and Emilio Mu{\\~{n}}oz{-}Velasco and Guido Sciavicco},\n\tBibsource = {dblp computer science bibliography, https://dblp.org},\n\tBiburl = {https://dblp.org/rec/bib/conf/time/BresolinCGMS18},\n\tBooktitle = {25th International Symposium on Temporal Representation and Reasoning, {TIME} 2018},\n\tDate-Added = {2018-10-19 12:50:05 +0000},\n\tDate-Modified = {2018-10-19 12:51:03 +0000},\n\tDoi = {10.4230/LIPIcs.TIME.2018.7},\n\tPages = {7:1--7:15},\n\tSeries = {LIPIcs},\n\tTimestamp = {Tue, 09 Oct 2018 13:57:40 +0200},\n\tTitle = {Extracting Interval Temporal Logic Rules: {A} First Approach},\n\tUrl = {10.4230/LIPIcs.TIME.2018.7},\n\tVolume = {120},\n\tYear = {2018},\n\tBdsk-Url-1 = {10.4230/LIPIcs.TIME.2018.7}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Formal Verification of Medical CPS: A Laser Incision Case Study.\n \n \n \n \n\n\n \n Geraldes, A. A.; Geretti, L.; Bresolin, D.; Muradore, R.; Fiorini, P.; Mattos, L. S.; and Villa, T.\n\n\n \n\n\n\n ACM Transactions on Cyber-Physical Systems (TCPS), 2(4): 35:1–35:29. 2018.\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n \n doi\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
@article{tcps2018,\n\tAuthor = {Andre A. Geraldes and Luca Geretti and Davide Bresolin and Riccardo Muradore and Paolo Fiorini and Leonardo S. Mattos and Tiziano Villa},\n\tBibsource = {dblp computer science bibliography, https://dblp.org},\n\tBiburl = {https://dblp.org/rec/bib/journals/tcps/GeraldesGBMFMV18},\n\tDate-Added = {2018-10-19 12:49:44 +0000},\n\tDate-Modified = {2018-10-19 12:54:42 +0000},\n\tDoi = {10.1145/3140237},\n\tJournal = {ACM Transactions on Cyber-Physical Systems (TCPS)},\n\tNumber = {4},\n\tPages = {35:1--35:29},\n\tTimestamp = {Thu, 18 Oct 2018 16:39:55 +0200},\n\tTitle = {Formal Verification of Medical {CPS:} {A} Laser Incision Case Study},\n\tUrl = {http://doi.acm.org/10.1145/3140237},\n\tVolume = {2},\n\tYear = {2018},\n\tBdsk-Url-1 = {http://doi.acm.org/10.1145/3140237},\n\tBdsk-Url-2 = {https://dx.doi.org/10.1145/3140237}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n On Sub-Propositional Fragments of Modal Logic.\n \n \n \n \n\n\n \n Bresolin, D.; Muñoz-Velasco, E.; and Sciavicco, G.\n\n\n \n\n\n\n Logical Methods in Computer Science, 14(2). 2018.\n \n\n\n\n
\n\n\n\n \n \n \"OnPaper\n  \n \n\n \n \n doi\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
@article{lmcs2018,\n\tAuthor = {Davide Bresolin and Emilio Mu{\\~{n}}oz{-}Velasco and Guido Sciavicco},\n\tBibsource = {dblp computer science bibliography, https://dblp.org},\n\tBiburl = {https://dblp.org/rec/bib/journals/lmcs/BresolinMS18},\n\tDate-Added = {2018-10-19 12:49:18 +0000},\n\tDate-Modified = {2018-10-19 12:49:25 +0000},\n\tDoi = {10.23638/LMCS-14(2:16)2018},\n\tJournal = {Logical Methods in Computer Science},\n\tNumber = {2},\n\tTimestamp = {Thu, 09 Aug 2018 10:30:38 +0200},\n\tTitle = {On Sub-Propositional Fragments of Modal Logic},\n\tUrl = {10.23638/LMCS-14(2:16)2018},\n\tVolume = {14},\n\tYear = {2018},\n\tBdsk-Url-1 = {10.23638/LMCS-14(2:16)2018}}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2017\n \n \n (6)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Parametric formal verification: the robotic paint spraying case study.\n \n \n \n \n\n\n \n Geretti, L.; Muradore, R.; Bresolin, D.; Fiorini, P.; and Villa, T.\n\n\n \n\n\n\n In Proc. of the 20th IFAC World Congress, volume 50, Issue 1, of IFAC-PapersOnLine, pages 9248–9253, 2017. \n \n\n\n\n
\n\n\n\n \n \n \"ParametricPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \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\n\n\n
\n
@inproceedings{ifac2017,\n\tAbstract = {The design of robots in industrial automation is based on classical control theory approaches. Recently, formal verification methodologies have been introduced in the design flow, due to their ability of analyzing the model of the robot-environment system in a conservative way. In this paper we specifically explore the analysis of system parameters within a continuous space, by developing an extension of the tool Ariadne for reachability analysis of hybrid automata. Under this framework, the system takes the form of a composition of automata which model discrete control parts that operate in a continuous environment. In particular, the dynamics of the system includes parameters, i.e., unspecified constants for which we want to observe the effect on the dynamics, with the purpose of finding optimal design values. As a case study for this methodology, we consider a robotic paint sprayer, in which we use Ariadne to study the effect of choosing different values of a parameter that represents a point of observation for the system. Using the information gathered from this automated analysis, we provide an answer to the problem of optimizing the surface spraying speed while respecting a given measure of spraying quality.},\n\tAuthor = {Luca Geretti and Riccardo Muradore and Davide Bresolin and Paolo Fiorini and Tiziano Villa},\n\tBooktitle = {Proc. of the 20th IFAC World Congress},\n\tDate-Added = {2019-04-03 08:46:23 +0000},\n\tDate-Modified = {2019-04-03 08:47:41 +0000},\n\tDoi = {10.1016/j.ifacol.2017.08.1287},\n\tIssn = {2405-8963},\n\tKeywords = {Parametrization, Formal verification, Robotics, Hybrid systems, Nonlinear systems, Reachability, Interval arithmetics},\n\tPages = {9248--9253},\n\tSeries = {IFAC-PapersOnLine},\n\tTitle = {Parametric formal verification: the robotic paint spraying case study},\n\tUrl = {http://www.sciencedirect.com/science/article/pii/S2405896317318050},\n\tVolume = {50, Issue 1},\n\tYear = {2017},\n\tBdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S2405896317318050},\n\tBdsk-Url-2 = {10.1016/j.ifacol.2017.08.1287}}\n\n
\n
\n\n\n
\n The design of robots in industrial automation is based on classical control theory approaches. Recently, formal verification methodologies have been introduced in the design flow, due to their ability of analyzing the model of the robot-environment system in a conservative way. In this paper we specifically explore the analysis of system parameters within a continuous space, by developing an extension of the tool Ariadne for reachability analysis of hybrid automata. Under this framework, the system takes the form of a composition of automata which model discrete control parts that operate in a continuous environment. In particular, the dynamics of the system includes parameters, i.e., unspecified constants for which we want to observe the effect on the dynamics, with the purpose of finding optimal design values. As a case study for this methodology, we consider a robotic paint sprayer, in which we use Ariadne to study the effect of choosing different values of a parameter that represents a point of observation for the system. Using the information gathered from this automated analysis, we provide an answer to the problem of optimizing the surface spraying speed while respecting a given measure of spraying quality.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Finite Satisfiability of Interval Temporal Logic Formulas with Multi-Objective Metaheuristics.\n \n \n \n \n\n\n \n Bresolin, D.; Jiménez, F.; Sánchez, G.; and Sciavicco, G.\n\n\n \n\n\n\n Multiple-Valued Logic and Soft Computing, 28(2-3): 217–249. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"FinitePaper\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
@article{mvlsc17,\n\tAuthor = {Davide Bresolin and Fernando Jim{\\'{e}}nez and Gracia S{\\'{a}}nchez and Guido Sciavicco},\n\tBibsource = {dblp computer science bibliography, http://dblp.org},\n\tBiburl = {http://dblp.org/rec/bib/journals/mvl/BresolinJSS17},\n\tDate-Added = {2019-04-03 08:30:57 +0000},\n\tDate-Modified = {2019-04-03 08:30:57 +0000},\n\tJournal = {Multiple-Valued Logic and Soft Computing},\n\tNumber = {2-3},\n\tPages = {217--249},\n\tTimestamp = {Fri, 13 Jan 2017 07:35:54 +0100},\n\tTitle = {Finite Satisfiability of Interval Temporal Logic Formulas with Multi-Objective Metaheuristics},\n\tUrl = {http://www.oldcitypublishing.com/journals/mvlsc-home/mvlsc-issue-contents/mvlsc-volume-28-number-2-3-2017/mvlsc-28-2-3-p-217-249/},\n\tVolume = {28},\n\tYear = {2017},\n\tBdsk-Url-1 = {http://www.oldcitypublishing.com/journals/mvlsc-home/mvlsc-issue-contents/mvlsc-volume-28-number-2-3-2017/mvlsc-28-2-3-p-217-249/}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Ongoing Work on Automated Verification of Noisy Nonlinear Systems with Ariadne.\n \n \n \n\n\n \n Geretti, L.; Bresolin, D.; Collins, P.; Gonzalez, S. Z.; and Villa, T.\n\n\n \n\n\n\n In ICTSS, volume 10533, of Lecture Notes in Computer Science, pages 313–319, 2017. Springer\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
@inproceedings{ictss2017,\n\tAuthor = {Luca Geretti and Davide Bresolin and Pieter Collins and Sanja Zivanovic Gonzalez and Tiziano Villa},\n\tBooktitle = {{ICTSS}},\n\tDate-Added = {2019-04-02 15:46:51 +0000},\n\tDate-Modified = {2019-04-02 15:47:01 +0000},\n\tPages = {313--319},\n\tPublisher = {Springer},\n\tSeries = {Lecture Notes in Computer Science},\n\tTitle = {Ongoing Work on Automated Verification of Noisy Nonlinear Systems with Ariadne},\n\tVolume = {10533},\n\tYear = {2017}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Fast(er) Reasoning in Interval Temporal Logic.\n \n \n \n \n\n\n \n Bresolin, D.; Muñoz-Velasco, E.; and Sciavicco, G.\n\n\n \n\n\n\n In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82, of Leibniz International Proceedings in Informatics (LIPIcs), pages 17:1–17:17, Stoccolma, Svezia, 2017. \n \n\n\n\n
\n\n\n\n \n \n \"Fast(er)Paper\n  \n \n\n \n \n doi\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
@inproceedings{csl2017,\n\tAddress = {Stoccolma, Svezia},\n\tAnnote = {Keywords: Temporal Logic, Horn Fragments, Satisfiability, Complexity},\n\tAuthor = {Davide Bresolin and Emilio Mu{\\~n}oz-Velasco and Guido Sciavicco},\n\tBooktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},\n\tDate-Added = {2017-09-25 13:43:15 +0000},\n\tDate-Modified = {2017-09-25 13:45:33 +0000},\n\tDoi = {10.4230/LIPIcs.CSL.2017.17},\n\tIsbn = {978-3-95977-045-3},\n\tIssn = {1868-8969},\n\tPages = {17:1--17:17},\n\tSeries = {Leibniz International Proceedings in Informatics (LIPIcs)},\n\tTitle = {{Fast(er) Reasoning in Interval Temporal Logic}},\n\tUrl = {http://drops.dagstuhl.de/opus/volltexte/2017/7678},\n\tUrn = {urn:nbn:de:0030-drops-76782},\n\tVolume = {82},\n\tYear = {2017},\n\tBdsk-Url-1 = {http://drops.dagstuhl.de/opus/volltexte/2017/7678},\n\tBdsk-Url-2 = {http://dx.doi.org/10.4230/LIPIcs.CSL.2017.17}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Most General Property-Preserving Updates.\n \n \n \n \n\n\n \n Bresolin, D.; and Lanese, I.\n\n\n \n\n\n\n In Proc. of the 11th International Conference on Language and Automata Theory and Applications, LATA 2017, volume 10168, of LNCS, pages 367–379, Umeå, Svezia, 6-9 Marzo 2017. \n \n\n\n\n
\n\n\n\n \n \n \"MostPaper\n  \n \n\n \n \n doi\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
@inproceedings{lata2017,\n\tAddress = {Ume{\\aa}, Svezia},\n\tAuthor = {Davide Bresolin and Ivan Lanese},\n\tBibsource = {dblp computer science bibliography, http://dblp.org},\n\tBiburl = {http://dblp.uni-trier.de/rec/bib/conf/lata/BresolinL17},\n\tBooktitle = {Proc. of the 11th International Conference on Language and Automata Theory and Applications, {LATA} 2017},\n\tDate-Added = {2017-09-25 12:20:25 +0000},\n\tDate-Modified = {2017-09-25 13:15:18 +0000},\n\tDoi = {10.1007/978-3-319-53733-7_27},\n\tMonth = {6-9 Marzo},\n\tPages = {367--379},\n\tSeries = {LNCS},\n\tTimestamp = {Wed, 24 May 2017 08:29:26 +0200},\n\tTitle = {Most General Property-Preserving Updates},\n\tUrl = {10.1007/978-3-319-53733-7_27},\n\tVolume = {10168},\n\tYear = {2017},\n\tBdsk-Url-1 = {10.1007/978-3-319-53733-7_27},\n\tBdsk-Url-2 = {http://dx.doi.org/10.1007/978-3-319-53733-7_27}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Horn Fragments of the Halpern-Shoham Interval Temporal Logic.\n \n \n \n \n\n\n \n Bresolin, D.; Kurucz, A.; Muñoz-Velasco, E.; Ryzhikov, V.; Sciavicco, G.; and Zakharyaschev, M.\n\n\n \n\n\n\n ACM Trans. Comput. Log., 18(3): 22:1–22:39. 2017.\n \n\n\n\n
\n\n\n\n \n \n \"HornPaper\n  \n \n\n \n \n doi\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
@article{tocl2017,\n\tAuthor = {Davide Bresolin and Agi Kurucz and Emilio Mu{\\~{n}}oz{-}Velasco and Vladislav Ryzhikov and Guido Sciavicco and Michael Zakharyaschev},\n\tBibsource = {dblp computer science bibliography, http://dblp.org},\n\tBiburl = {http://dblp.uni-trier.de/rec/bib/journals/tocl/BresolinKMRSZ17},\n\tDate-Added = {2017-09-25 12:17:07 +0000},\n\tDate-Modified = {2017-09-25 12:17:16 +0000},\n\tDoi = {10.1145/3105909},\n\tJournal = {{ACM} Trans. Comput. Log.},\n\tNumber = {3},\n\tPages = {22:1--22:39},\n\tTimestamp = {Wed, 30 Aug 2017 15:38:05 +0200},\n\tTitle = {Horn Fragments of the Halpern-Shoham Interval Temporal Logic},\n\tUrl = {http://doi.acm.org/10.1145/3105909},\n\tVolume = {18},\n\tYear = {2017},\n\tBdsk-Url-1 = {http://doi.acm.org/10.1145/3105909},\n\tBdsk-Url-2 = {http://dx.doi.org/10.1145/3105909}}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2016\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n On the Expressive Power of Sub-Propositional Fragments of Modal Logic.\n \n \n \n \n\n\n \n Bresolin, D.; Muñoz-Velasco, E.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016., volume 226, of EPTCS, pages 91–104, 2016. \n \n\n\n\n
\n\n\n\n \n \n \"OnPaper\n  \n \n\n \n \n doi\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
@inproceedings{gandalf2016,\n\tAuthor = {Davide Bresolin and Emilio Mu{\\~{n}}oz{-}Velasco and Guido Sciavicco},\n\tBibsource = {dblp computer science bibliography, http://dblp.org},\n\tBiburl = {http://dblp.org/rec/bib/journals/corr/BresolinMS16},\n\tBooktitle = {Proc. of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016.},\n\tDate-Added = {2019-04-03 08:30:57 +0000},\n\tDate-Modified = {2019-04-03 08:30:57 +0000},\n\tDoi = {10.4204/EPTCS.226.7},\n\tPages = {91--104},\n\tSeries = {{EPTCS}},\n\tTimestamp = {Wed, 03 May 2017 14:47:56 +0200},\n\tTitle = {On the Expressive Power of Sub-Propositional Fragments of Modal Logic},\n\tUrl = {10.4204/EPTCS.226.7},\n\tVolume = {226},\n\tYear = {2016},\n\tBdsk-Url-1 = {10.4204/EPTCS.226.7},\n\tBdsk-Url-2 = {http://dx.doi.org/10.4204/EPTCS.226.7}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n On the Complexity of Fragments of Horn Modal Logics.\n \n \n \n \n\n\n \n Bresolin, D.; Muñoz-Velasco, E.; and Sciavicco, G.\n\n\n \n\n\n\n In 23rd International Symposium on Temporal Representation and Reasoning, TIME 2016, Kongens Lyngby, Denmark, October 17-19, 2016, pages 186–195, 2016. IEEE Computer Society\n \n\n\n\n
\n\n\n\n \n \n \"OnPaper\n  \n \n\n \n \n doi\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
@inproceedings{time2016,\n\tAuthor = {Davide Bresolin and Emilio Mu{\\~{n}}oz{-}Velasco and Guido Sciavicco},\n\tBibsource = {dblp computer science bibliography, http://dblp.org},\n\tBiburl = {http://dblp.org/rec/bib/conf/time/BresolinMS16},\n\tBooktitle = {23rd International Symposium on Temporal Representation and Reasoning, {TIME} 2016, Kongens Lyngby, Denmark, October 17-19, 2016},\n\tDate-Added = {2019-04-03 08:30:57 +0000},\n\tDate-Modified = {2019-04-03 08:30:57 +0000},\n\tDoi = {10.1109/TIME.2016.27},\n\tPages = {186--195},\n\tPublisher = {{IEEE} Computer Society},\n\tTimestamp = {Thu, 25 May 2017 00:39:53 +0200},\n\tTitle = {On the Complexity of Fragments of Horn Modal Logics},\n\tUrl = {10.1109/TIME.2016.27},\n\tYear = {2016},\n\tBdsk-Url-1 = {10.1109/TIME.2016.27},\n\tBdsk-Url-2 = {http://dx.doi.org/10.1109/TIME.2016.27}}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2015\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Formal verification of robotic surgery tasks by reachability analysis.\n \n \n \n \n\n\n \n Bresolin, D.; Geretti, L.; Muradore, R.; Fiorini, P.; and Villa, T.\n\n\n \n\n\n\n Microprocessors and Microsystems, 39(8): 836 - 842. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"FormalPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n\n\n\n
\n
@article{micpro2015,\n\tAbstract = {Abstract In this paper we discuss the application of formal methods for the verification of properties of control systems designed for autonomous robotic systems. We illustrate our proposal in the context of surgery by considering the automatic execution of a simple action such as puncturing. To prove that a sequence of subtasks planned on pre-operative data can successfully accomplish the surgical operation despite model uncertainties, we specify the problem by using hybrid automata. We express the requirements of interest as questions about reachability properties of the hybrid automaton model. Then, we use the tool Ariadne to study how the choice of the control parameters and the measurement error affect the safety of the system. },\n\tAuthor = {Davide Bresolin and Luca Geretti and Riccardo Muradore and Paolo Fiorini and Tiziano Villa},\n\tDate-Added = {2015-12-03 13:46:47 +0000},\n\tDate-Modified = {2019-04-05 12:45:38 +0000},\n\tDoi = {10.1016/j.micpro.2015.10.006},\n\tFpage = 836,\n\tIssn = {0141-9331},\n\tJournal = {Microprocessors and Microsystems},\n\tKeywords = {Surgical robotics},\n\tLpage = 842,\n\tNumber = {8},\n\tNumpages = {7},\n\tPages = {836 - 842},\n\tPublisher = {Elsevier},\n\tTitle = {Formal verification of robotic surgery tasks by reachability analysis},\n\tUrl = {http://www.sciencedirect.com/science/article/pii/S014193311500160X},\n\tVolume = {39},\n\tYear = {2015},\n\tBdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S014193311500160X},\n\tBdsk-Url-2 = {http://dx.doi.org/10.1016/j.micpro.2015.10.006}}\n\n
\n
\n\n\n
\n Abstract In this paper we discuss the application of formal methods for the verification of properties of control systems designed for autonomous robotic systems. We illustrate our proposal in the context of surgery by considering the automatic execution of a simple action such as puncturing. To prove that a sequence of subtasks planned on pre-operative data can successfully accomplish the surgical operation despite model uncertainties, we specify the problem by using hybrid automata. We express the requirements of interest as questions about reachability properties of the hybrid automaton model. Then, we use the tool Ariadne to study how the choice of the control parameters and the measurement error affect the safety of the system. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Platform-Based Design Methodology With Contracts and Related Tools for the Design of Cyber-Physical Systems.\n \n \n \n \n\n\n \n Nuzzo, P.; Sangiovanni-Vincentelli, A.; Bresolin, D.; Geretti, L.; and Villa, T.\n\n\n \n\n\n\n Proceedings of the IEEE, 103(11): 2104–2132. 2015.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\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
@article{IEEEProc2015,\n\tArt_Number = {7268792},\n\tAuthor = {Nuzzo, P. and Sangiovanni-Vincentelli, A.L. and Bresolin, D. and Geretti, L. and Villa, T.},\n\tDate-Added = {2015-12-03 13:35:40 +0000},\n\tDate-Modified = {2015-12-03 13:36:16 +0000},\n\tDocument_Type = {Article},\n\tFpage = 2104,\n\tJournal = {Proceedings of the IEEE},\n\tLpage = 2132,\n\tNumber = {11},\n\tNumpages = 28,\n\tPages = {2104--2132},\n\tPublisher = {IEEE},\n\tSource = {Scopus},\n\tTitle = {A Platform-Based Design Methodology With Contracts and Related Tools for the Design of Cyber-Physical Systems},\n\tUrl = {http://www.scopus.com/inward/record.url?eid=2-s2.0-84946499411&partnerID=40&md5=f520f7ffa70c24c653c565c299ada445},\n\tVolume = {103},\n\tYear = {2015},\n\tBdsk-Url-1 = {http://www.scopus.com/inward/record.url?eid=2-s2.0-84946499411&partnerID=40&md5=f520f7ffa70c24c653c565c299ada445},\n\tBdsk-Url-2 = {http://dx.doi.org/10.1109/JPROC.2015.2453253}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n On the Complexity of Fragments of the Modal Logic of Allen's Relations over Dense Structures.\n \n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Montanari, A.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of 9th International Conference (LATA 2015), volume 8977, of Lecture Notes in Computer Science, pages 511–523, Nizza, Francia, 2015. Springer\n \n\n\n\n
\n\n\n\n \n \n \"OnPaper\n  \n \n\n \n \n doi\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
@inproceedings{lata2015,\n\tAddress = {Nizza, Francia},\n\tAuthor = {Davide Bresolin and Dario {Della Monica} and Angelo Montanari and Pietro Sala and Guido Sciavicco},\n\tBibsource = {dblp computer science bibliography, http://dblp.org},\n\tBiburl = {http://dblp.uni-trier.de/rec/bib/conf/lata/BresolinMMSS15},\n\tBooktitle = {Proc. of 9th International Conference (LATA 2015)},\n\tDate-Added = {2015-05-11 08:48:29 +0000},\n\tDate-Modified = {2015-05-11 08:49:09 +0000},\n\tDoi = {10.1007/978-3-319-15579-1_40},\n\tPages = {511--523},\n\tPublisher = {Springer},\n\tSeries = {Lecture Notes in Computer Science},\n\tTimestamp = {Tue, 24 Feb 2015 14:58:39 +0100},\n\tTitle = {On the Complexity of Fragments of the Modal Logic of Allen's Relations over Dense Structures},\n\tUrl = {http://dx.doi.org/10.1007/978-3-319-15579-1_40},\n\tVolume = {8977},\n\tYear = {2015},\n\tBdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-319-15579-1_40}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Formal Verification Applied to Robotic Surgery.\n \n \n \n\n\n \n Bresolin, D.; Geretti, L.; Muradore, R.; Fiorini, P.; and Villa, T.\n\n\n \n\n\n\n In Coordination Control of Distributed Systems, volume 456, of Lecture Notes in Control and Information Sciences, pages 347–355. Springer International Publishing, 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
@incollection{c4cbook2015b,\n\tAuthor = {Bresolin, Davide and Geretti, Luca and Muradore, Riccardo and Fiorini, Paolo and Villa, Tiziano},\n\tBooktitle = {Coordination Control of Distributed Systems},\n\tDate-Added = {2015-05-11 08:43:09 +0000},\n\tDate-Modified = {2015-05-11 08:43:23 +0000},\n\tPages = {347--355},\n\tPublisher = {Springer International Publishing},\n\tSeries = {Lecture Notes in Control and Information Sciences},\n\tTitle = {Formal Verification Applied to Robotic Surgery},\n\tVolume = {456},\n\tYear = {2015}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An Introduction to the Verification of Hybrid Systems Using Ariadne.\n \n \n \n\n\n \n Bresolin, D.; Geretti, L.; Villa, T.; and Collins, P.\n\n\n \n\n\n\n In Coordination Control of Distributed Systems, volume 456, of Lecture Notes in Control and Information Sciences, pages 339–346. Springer, 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
@incollection{c4cbook2015a,\n\tAuthor = {Bresolin, Davide and Geretti, Luca and Villa, Tiziano and Collins, Pieter},\n\tBooktitle = {Coordination Control of Distributed Systems},\n\tDate-Added = {2015-05-11 08:41:35 +0000},\n\tDate-Modified = {2015-05-11 08:42:43 +0000},\n\tPages = {339--346},\n\tPublisher = {Springer},\n\tSeries = {Lecture Notes in Control and Information Sciences},\n\tTitle = {An Introduction to the Verification of Hybrid Systems Using {Ariadne}},\n\tVolume = {456},\n\tYear = {2015}}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2014\n \n \n (9)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Interval temporal logics over strongly discrete linear orders: Expressiveness and complexity.\n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Montanari, A.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n Theoretical Computer Science, 560: 269–291. 2014.\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
@article{tcs2014,\n\tAuthor = {D. Bresolin and D. {Della Monica} and A. Montanari and P. Sala and G. Sciavicco},\n\tDate-Added = {2014-08-26 18:15:47 +0200},\n\tDate-Modified = {2015-12-03 13:34:43 +0000},\n\tFpage = 269,\n\tGcited = {1},\n\tJournal = {Theoretical Computer Science},\n\tLpage = 291,\n\tNumpages = 23,\n\tPages = {269--291},\n\tPublisher = {Springer},\n\tTitle = {Interval temporal logics over strongly discrete linear orders: Expressiveness and complexity},\n\tVolume = {560},\n\tYear = {2014},\n\tBdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S0304397514002552},\n\tBdsk-Url-2 = {http://dx.doi.org/10.1016/j.tcs.2014.03.033}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Sub-Propositional Fragments of the Interval Temporal Logic of Allen's Relations.\n \n \n \n\n\n \n Bresolin, D.; Muñoz-Velasco, E.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of JELIA 2014: 14th European Conference on Logics in Artificial Intelligence, volume 8761, of LNCS, pages 122-136, Madeira, Portogallo, September 2014. Springer\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
@inproceedings{jelia2014,\n\tAddress = {Madeira, Portogallo},\n\tAuthor = {D. Bresolin and E. Mu{\\~{n}}oz-Velasco and G. Sciavicco},\n\tBooktitle = {Proc. of JELIA 2014: 14th European Conference on Logics in Artificial Intelligence},\n\tDate-Added = {2014-07-14 17:01:37 +0200},\n\tDate-Modified = {2015-08-18 15:33:40 +0000},\n\tMonth = sep,\n\tPages = {122-136},\n\tPublisher = {Springer},\n\tSeries = {LNCS},\n\tTitle = {Sub-Propositional Fragments of the Interval Temporal Logic of Allen's Relations},\n\tVolume = {8761},\n\tYear = {2014}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n DL-Lite and Interval Temporal Logics: a Marriage Proposal.\n \n \n \n\n\n \n Artale, A.; Bresolin, D.; Montanari, A.; Sciavicco, G.; and Ryzhikov, V.\n\n\n \n\n\n\n In Proc. of ECAI 2014: 21st European Conference on Artificial Intelligence, volume 263, of Frontiers in Artificial Intelligence and Applications, pages 957-958, Praga, Repubblica Ceca, August 2014. IOS Press\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
@inproceedings{ecai2014,\n\tAddress = {Praga, Repubblica Ceca},\n\tAuthor = {A. Artale and D. Bresolin and A. Montanari and G. Sciavicco and V. Ryzhikov},\n\tBooktitle = {Proc. of ECAI 2014: 21st European Conference on Artificial Intelligence},\n\tDate-Added = {2014-07-14 16:58:07 +0200},\n\tDate-Modified = {2014-08-27 10:18:09 +0200},\n\tMonth = aug,\n\tPages = {957-958},\n\tPublisher = {IOS Press},\n\tSeries = {Frontiers in Artificial Intelligence and Applications},\n\tTitle = {{DL-Lite} and {Interval Temporal Logics}: a Marriage Proposal},\n\tVolume = {263},\n\tYear = {2014}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Verification of robotic surgery tasks by reachability analysis: a comparison of tools.\n \n \n \n\n\n \n Bresolin, D.; Geretti, L.; Muradore, R.; Fiorini, P.; and Villa, T.\n\n\n \n\n\n\n In Proc. of the 17th Euromicro Conference on Digital System Design (DSD2014), Verona, August 2014. IEEE Comp. Society Press\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
@inproceedings{dsd2014,\n\tAddress = {Verona},\n\tAuthor = {D. Bresolin and L. Geretti and R. Muradore and P. Fiorini and T. Villa},\n\tBooktitle = {Proc. of the 17th Euromicro Conference on Digital System Design (DSD2014)},\n\tDate-Added = {2014-07-14 16:53:56 +0200},\n\tDate-Modified = {2014-08-27 10:21:44 +0200},\n\tMonth = aug,\n\tPublisher = {IEEE Comp. Society Press},\n\tTitle = {Verification of robotic surgery tasks by reachability analysis: a comparison of tools},\n\tYear = {2014}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power.\n \n \n \n\n\n \n Bresolin, D.; El-Fakih, K.; Villa, T.; and Yevtushenko, N.\n\n\n \n\n\n\n In Proc. of GandALF 2014: 5th International Symposium on Games, Automata, Logics and Formal Verification, volume 161, of EPTCS, pages 203–216, Verona, Settembre 2014. Open Publishing Association\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
@inproceedings{gandalf2014,\n\tAddress = {Verona},\n\tAuthor = {Bresolin, D. and El-Fakih, K. and Villa, T. and Yevtushenko, N.},\n\tBooktitle = {Proc. of GandALF 2014: 5th International Symposium on Games, Automata, Logics and Formal Verification},\n\tDate-Added = {2014-07-14 16:50:40 +0200},\n\tDate-Modified = {2014-08-27 10:20:00 +0200},\n\tMonth = {Settembre},\n\tPages = {203--216},\n\tPublisher = {Open Publishing Association},\n\tSeries = {EPTCS},\n\tTitle = {Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power},\n\tVolume = {161},\n\tYear = {2014},\n\tBdsk-Url-1 = {http://dx.doi.org/10.4204/EPTCS.119.9}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Application of Contract-Based Verification Techniques for Hybrid Automata to Surgical Robotic Systems.\n \n \n \n\n\n \n Schreiter, L.; Bresolin, D.; Capiluppi, M.; Raczkowsky, J.; Fiorini, P.; and Woern, H.\n\n\n \n\n\n\n In Proc. of 13th European Control Conference (ECC14), pages 2310-2315, Strasburgo, Francia, Giugno 2014. IEEE\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
@inproceedings{ecc2014,\n\tAddress = {Strasburgo, Francia},\n\tAuthor = {Schreiter, L. and Bresolin, D. and Capiluppi, M. and Raczkowsky, J. and Fiorini, P. and Woern, H.},\n\tBooktitle = {Proc. of 13th European Control Conference (ECC14)},\n\tDate-Added = {2014-07-14 16:45:45 +0200},\n\tDate-Modified = {2014-08-27 12:27:00 +0200},\n\tMonth = {Giugno},\n\tPages = {2310-2315},\n\tPublisher = {IEEE},\n\tTitle = {Application of Contract-Based Verification Techniques for Hybrid Automata to Surgical Robotic Systems},\n\tYear = {2014}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The dark side of interval temporal logic: marking the undecidability border.\n \n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Goranko, V.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n Annals of Mathematics and Artificial Intelligence, 71(1-3): 41-83. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\n  \n \n\n \n \n doi\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{amai2014b,\n\tAuthor = {Bresolin, D. and {Della Monica}, D. and Goranko, V. and Montanari, A. and Sciavicco, G.},\n\tDate-Added = {2014-07-14 16:31:47 +0200},\n\tDate-Modified = {2014-08-27 13:41:42 +0200},\n\tDoi = {10.1007/s10472-013-9376-4},\n\tFpage = 41,\n\tGcited = {1},\n\tIssn = {1012-2443},\n\tJournal = {Annals of Mathematics and Artificial Intelligence},\n\tKeywords = {Interval temporal logic; Undecidability; Tiling problems; 03B44; 03D35; 68T27; 05B45},\n\tLanguage = {English},\n\tLpage = 83,\n\tNumber = {1-3},\n\tNumpages = 43,\n\tPages = {41-83},\n\tPublisher = {Springer International Publishing},\n\tTitle = {The dark side of interval temporal logic: marking the undecidability border},\n\tUrl = {http://dx.doi.org/10.1007/s10472-013-9376-4},\n\tVolume = {71},\n\tYear = {2014},\n\tBdsk-Url-1 = {http://dx.doi.org/10.1007/s10472-013-9376-4}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT.\n \n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n Annals of Mathematics and Artificial Intelligence, 71(1-3): 11-39. 2014.\n \n\n\n\n
\n\n\n\n \n \n \"ThePaper\n  \n \n\n \n \n doi\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{amai2014a,\n\tAuthor = {Bresolin, D. and {Della Monica}, D. and Montanari, A. and Sciavicco, G.},\n\tDate-Added = {2014-07-14 16:31:23 +0200},\n\tDate-Modified = {2014-07-14 16:34:50 +0200},\n\tDoi = {10.1007/s10472-013-9337-y},\n\tFpage = 11,\n\tIssn = {1012-2443},\n\tJournal = {Annals of Mathematics and Artificial Intelligence},\n\tKeywords = {Interval temporal logic; Tableau methods; Decidability; Complexity; 03B44; 03B25; 68T15; 68T27},\n\tLanguage = {English},\n\tLpage = 39,\n\tNumber = {1-3},\n\tNumpages = 29,\n\tPages = {11-39},\n\tPublisher = {Springer International Publishing},\n\tTitle = {The light side of interval temporal logic: the {Bernays-Sch\\"{o}nfinkel} fragment of {CDT}},\n\tUrl = {http://dx.doi.org/10.1007/s10472-013-9337-y},\n\tVolume = {71},\n\tYear = {2014},\n\tBdsk-Url-1 = {http://dx.doi.org/10.1007/s10472-013-9337-y}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Assume-guarantee verification of nonlinear hybrid systems with ARIADNE.\n \n \n \n\n\n \n Benvenuti, L.; Bresolin, D.; Collins, P.; Ferrari, A.; Geretti, L.; and Villa, T.\n\n\n \n\n\n\n Int. J. Robust. Nonlinear Control, 24(4): 699-724. 2014.\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
@article{ijrnc2014,\n\tAuthor = {L. Benvenuti and D. Bresolin and P. Collins and A. Ferrari and L. Geretti and T. Villa},\n\tDate-Added = {2014-07-14 16:29:09 +0200},\n\tDate-Modified = {2014-08-27 13:31:51 +0200},\n\tFpage = 699,\n\tGcited = {3},\n\tJournal = {Int. J. Robust. Nonlinear Control},\n\tLpage = 724,\n\tNumber = {4},\n\tNumpages = 26,\n\tPages = {699-724},\n\tPublisher = {Wiley},\n\tTitle = {Assume-guarantee verification of nonlinear hybrid systems with {ARIADNE}},\n\tVolume = {24},\n\tYear = {2014},\n\tBdsk-Url-1 = {http://dx.doi.org/10.1002/rnc.2914}}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2013\n \n \n (8)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n A framework for Fault Diagnosis of Hybrid Systems based on Predicate Abstractions.\n \n \n \n\n\n \n Bresolin, D.; and Capiluppi, M.\n\n\n \n\n\n\n In Proc. of 2nd International Conference on Control and Fault-Tolerant Systems (SysTol'13), pages 802-807, Nizza, Francia, Ottobre 2013. IEEE Comp. Society Press\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
@inproceedings{systol2013,\n\tAddress = {Nizza, Francia},\n\tAuthor = {D. Bresolin and M. Capiluppi},\n\tBooktitle = {Proc. of 2nd International Conference on Control and Fault-Tolerant Systems (SysTol'13)},\n\tDate-Added = {2013-07-24 15:54:14 +0200},\n\tDate-Modified = {2014-07-14 16:41:05 +0200},\n\tMonth = {Ottobre},\n\tPages = {802-807},\n\tPublisher = {IEEE Comp. Society Press},\n\tTitle = {A framework for {Fault Diagnosis of Hybrid Systems based on Predicate Abstractions}},\n\tYear = {2013}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n HyLTL: a temporal logic for model checking hybrid systems.\n \n \n \n\n\n \n Bresolin, D.\n\n\n \n\n\n\n In Proc. of 3rd International Workshop on Hybrid Autonomous Systems (HAS 2013), of EPTCS, pages 73—84, 2013. Open Publishing Association\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
@inproceedings{has2013,\n\tAuthor = {D. Bresolin},\n\tBooktitle = {Proc. of 3rd International Workshop on Hybrid Autonomous Systems (HAS 2013)},\n\tDate-Added = {2013-07-24 15:50:56 +0200},\n\tDate-Modified = {2014-08-27 13:32:21 +0200},\n\tGcited = {3},\n\tPages = {73---84},\n\tPublisher = {Open Publishing Association},\n\tSeries = {EPTCS},\n\tTitle = {{HyLTL}: a temporal logic for model checking hybrid systems},\n\tYear = {2013}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Finite satisfiability of propositional interval logic formulas with multi-objective evolutionary algorithms.\n \n \n \n \n\n\n \n Bresolin, D.; Jiménez, F.; Sánchez, G.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of the 12th workshop on Foundations of genetic algorithms (FOGA2013), pages 25–36, Adelaide, Australia, Gennaio 2013. ACM\n \n\n\n\n
\n\n\n\n \n \n \"FinitePaper\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
@inproceedings{foga2013,\n\tAcmid = {2460243},\n\tAddress = {Adelaide, Australia},\n\tAuthor = {Bresolin, D. and Jim\\'{e}nez, F. and S\\'{a}nchez, G. and Sciavicco, G.},\n\tBooktitle = {Proc. of the 12th workshop on Foundations of genetic algorithms (FOGA2013)},\n\tDate-Added = {2013-07-24 15:47:10 +0200},\n\tDate-Modified = {2014-08-27 13:32:57 +0200},\n\tFpage = {25},\n\tGcited = {3},\n\tIsbn = {978-1-4503-1990-4},\n\tLocation = {Adelaide, Australia},\n\tLpage = {36},\n\tMonth = {Gennaio},\n\tNumpages = {6},\n\tPages = {25--36},\n\tPublisher = {ACM},\n\tScited = {1},\n\tTitle = {Finite satisfiability of propositional interval logic formulas with multi-objective evolutionary algorithms},\n\tUrl = {http://doi.acm.org/10.1145/2460239.2460243},\n\tYear = {2013},\n\tBdsk-Url-1 = {http://doi.acm.org/10.1145/2460239.2460243},\n\tBdsk-Url-2 = {http://dx.doi.org/10.1145/2460239.2460243}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A tableau system for right propositional neighborhood logic over finite linear orders: an implementation.\n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of the 22nd Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX2013), volume 8123, of LNCS, pages 74-80, Nancy, Francia, Settembre 2013. Springer\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
@inproceedings{tableaux2013,\n\tAddress = {Nancy, Francia},\n\tAuthor = {Bresolin, D. and {Della Monica}, D. and Montanari, A. and Sciavicco, G.},\n\tBooktitle = {Proc. of the 22nd Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX2013)},\n\tDate-Added = {2013-07-24 15:43:41 +0200},\n\tDate-Modified = {2014-08-27 13:33:43 +0200},\n\tGcited = {3},\n\tMonth = {Settembre},\n\tPages = {74-80},\n\tPublisher = {Springer},\n\tScited = {1},\n\tSeries = {LNCS},\n\tTitle = {A tableau system for right propositional neighborhood logic over finite linear orders: an implementation},\n\tVolume = {8123},\n\tYear = {2013}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Improving HyLTL model checking of hybrid systems.\n \n \n \n\n\n \n Bresolin, D.\n\n\n \n\n\n\n In Proc. of GandALF 2013: 4th International Symposium on Games, Automata, Logics and Formal Verification, volume 119, of EPTCS, pages 79–92, Borca di Cadore, Belluno, Agosto 2013. Open Publishing Association\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\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
@inproceedings{gandalf2013,\n\tAddress = {Borca di Cadore, Belluno},\n\tAuthor = {Bresolin, D.},\n\tBooktitle = {Proc. of GandALF 2013: 4th International Symposium on Games, Automata, Logics and Formal Verification},\n\tDate-Added = {2013-07-24 15:37:59 +0200},\n\tDate-Modified = {2014-08-27 13:41:20 +0200},\n\tDoi = {10.4204/EPTCS.119.9},\n\tFpage = {79},\n\tGcited = {1},\n\tLpage = {92},\n\tMonth = {Agosto},\n\tNumpages = {7},\n\tPages = {79--92},\n\tPublisher = {Open Publishing Association},\n\tSeries = {EPTCS},\n\tTitle = {Improving {HyLTL} model checking of hybrid systems},\n\tVolume = {119},\n\tYear = {2013},\n\tBdsk-Url-1 = {http://dx.doi.org/10.4204/EPTCS.119.9}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Game-Theoretic approach to Fault Diagnosis and Identification of Hybrid Systems.\n \n \n \n\n\n \n Bresolin, D.; and Capiluppi, M.\n\n\n \n\n\n\n Theoretical Computer Science, 493: 15—29. 2013.\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
@article{tcs2013a,\n\tAuthor = {D. Bresolin and M. Capiluppi},\n\tDate-Added = {2012-07-02 15:37:55 +0200},\n\tDate-Modified = {2014-08-27 13:36:26 +0200},\n\tFpage = {15},\n\tGcited = {2},\n\tJournal = {Theoretical Computer Science},\n\tLpage = {29},\n\tNumpages = {8},\n\tPages = {15---29},\n\tPublisher = {Elsevier},\n\tScited = {1},\n\tTitle = {A Game-Theoretic approach to Fault Diagnosis and Identification of Hybrid Systems},\n\tVolume = {493},\n\tYear = {2013}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Optimal decision procedures for MPNL over finite structures, the natural numbers, and the integers.\n \n \n \n\n\n \n Bresolin, D.; Montanari, A.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n Theoretical Computer Science, 493: 98—115. 2013.\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
@article{tcs2013b,\n\tAuthor = {D. Bresolin and A. Montanari and P. Sala and G. Sciavicco},\n\tDate-Added = {2012-01-27 16:11:25 +0100},\n\tDate-Modified = {2014-08-27 13:36:00 +0200},\n\tFpage = {98},\n\tGcited = {2},\n\tJournal = {Theoretical Computer Science},\n\tLpage = {115},\n\tNumpages = {9},\n\tPages = {98---115},\n\tPublisher = {Elsevier},\n\tTitle = {Optimal decision procedures for {MPNL} over finite structures, the natural numbers, and the integers},\n\tVolume = {493},\n\tYear = {2013}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Metric propositional neighborhood logics on natural numbers.\n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Goranko, V.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n Software & Systems Modeling, 12(2): 245–264. 2013.\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
@article{sosym2013,\n\tAffiliation = {University of Verona, Verona, Italy},\n\tAuthor = {D. Bresolin and {Della Monica}, D. and V. Goranko and A. Montanari and Sciavicco, G.},\n\tDate-Added = {2011-02-28 19:04:48 +0100},\n\tDate-Modified = {2014-08-27 13:11:44 +0200},\n\tFpage = {245},\n\tGcited = {16},\n\tIssn = {1619-1366},\n\tJournal = {Software \\& Systems Modeling},\n\tKeyword = {Computer Science},\n\tLpage = {264},\n\tNumber = {2},\n\tNumpages = {10},\n\tPages = {245--264},\n\tPublisher = {Springer},\n\tScited = {2},\n\tTitle = {Metric propositional neighborhood logics on natural numbers},\n\tVolume = {12},\n\tYear = {2013},\n\tBdsk-Url-1 = {http://dx.doi.org/10.1007/s10270-011-0195-y}}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2012\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis.\n \n \n \n\n\n \n Benvenuti, L.; Bresolin, D.; Collins, P.; Ferrari, A.; Geretti, L.; and Villa, T.\n\n\n \n\n\n\n In Proc. of 6th International workshop on Reachability Problems (RP'12), volume 7550, of LNCS, pages 79–91, Settembre 2012. Springer\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
@inproceedings{rp2012,\n\tAuthor = {L. Benvenuti and D. Bresolin and P. Collins and A. Ferrari and L. Geretti and T. Villa},\n\tBooktitle = {Proc. of 6th International workshop on Reachability Problems (RP'12)},\n\tDate-Added = {2012-07-03 16:01:36 +0200},\n\tDate-Modified = {2013-07-24 15:21:13 +0200},\n\tFpage = 79,\n\tLpage = 91,\n\tMonth = {Settembre},\n\tNumpages = 7,\n\tPages = {79--91},\n\tPublisher = {Springer},\n\tSeries = {LNCS},\n\tTitle = {Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis},\n\tVolume = {7550},\n\tYear = {2012}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Open Problems in Verification and Refinement of Autonomous Robotic Systems.\n \n \n \n\n\n \n Bresolin, D.; Di Guglielmo, L.; Geretti, L.; Muradore, R.; Fiorini, P.; and Villa, T.\n\n\n \n\n\n\n In Proc. of the 15th Euromicro Conference on Digital System Design (DSD2012), pages 469–476, Cesme-Izmir, Turchia, September 2012. IEEE Comp. Society Press\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
@inproceedings{dsd2012,\n\tAddress = {Cesme-Izmir, Turchia},\n\tAuthor = {D. Bresolin and L. {Di Guglielmo} and L. Geretti and R. Muradore and P. Fiorini and T. Villa},\n\tBooktitle = {Proc. of the 15th Euromicro Conference on Digital System Design (DSD2012)},\n\tDate-Added = {2012-07-02 19:43:22 +0200},\n\tDate-Modified = {2014-08-27 13:37:05 +0200},\n\tFpage = {469},\n\tGcited = {2},\n\tLpage = {476},\n\tMonth = sep,\n\tNumpages = {4},\n\tPages = {469--476},\n\tPublisher = {IEEE Comp. Society Press},\n\tScited = {2},\n\tTitle = {Open Problems in Verification and Refinement of Autonomous Robotic Systems},\n\tYear = {2012}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Interval Temporal Logics over Strongly Discrete Linear Orders: The Complete Picture.\n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Montanari, A.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of GandALF 2012: Third International Symposium on Games, Automata, Logics and Formal Verification, volume 96, of EPTCS, pages 155–168, Napoli, September 2012. Open Publishing Association\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
@inproceedings{gandalf2012,\n\tAddress = {Napoli},\n\tAuthor = {D. Bresolin and D. {Della Monica} and A. Montanari and P. Sala and G. Sciavicco},\n\tBooktitle = {Proc. of GandALF 2012: Third International Symposium on Games, Automata, Logics and Formal Verification},\n\tDate-Added = {2012-07-02 19:39:17 +0200},\n\tDate-Modified = {2014-08-27 13:27:11 +0200},\n\tFpage = {155},\n\tGcited = {6},\n\tLpage = {168},\n\tMonth = sep,\n\tNumpages = {7},\n\tPages = {155--168},\n\tPublisher = {Open Publishing Association},\n\tSeries = {EPTCS},\n\tTitle = {Interval Temporal Logics over Strongly Discrete Linear Orders: The Complete Picture},\n\tVolume = {96},\n\tYear = {2012}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Interval Temporal Logics over Finite Linear Orders: The Complete Picture.\n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Montanari, A.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of ECAI 2012: 20th European Conference on Artificial Intelligence, volume 242, of Frontiers in Artificial Intelligence and Applications, pages 199–204, Montpellier, Francia, August 2012. IOS Press\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
@inproceedings{ecai2012,\n\tAddress = {Montpellier, Francia},\n\tAuthor = {D. Bresolin and D. {Della Monica} and A. Montanari and P. Sala and G. Sciavicco},\n\tBooktitle = {Proc. of ECAI 2012: 20th European Conference on Artificial Intelligence},\n\tDate-Added = {2012-07-02 19:32:56 +0200},\n\tDate-Modified = {2014-08-27 13:14:16 +0200},\n\tFpage = {199},\n\tGcited = {12},\n\tLpage = {204},\n\tMonth = aug,\n\tNumpages = {3},\n\tPages = {199--204},\n\tPublisher = {IOS Press},\n\tScited = {1},\n\tSeries = {Frontiers in Artificial Intelligence and Applications},\n\tTitle = {Interval Temporal Logics over Finite Linear Orders: The Complete Picture},\n\tVolume = {242},\n\tYear = {2012}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Fault Diagnosis of Hybrid Systems: an Onboard Camera Model.\n \n \n \n\n\n \n Bresolin, D.; and Capiluppi, M.\n\n\n \n\n\n\n In Proc. of the 8th IFAC Symposium SAFEPROCESS-2012: Fault Detection, Supervision and Safety for Technical Processes, pages 714–719, Mexico City, Mexico, August 2012. Elsevier\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
@inproceedings{safeprocess2012,\n\tAddress = {Mexico City, Mexico},\n\tAuthor = {D. Bresolin and M. Capiluppi},\n\tBooktitle = {Proc. of the 8th IFAC Symposium SAFEPROCESS-2012: Fault Detection, Supervision and Safety for Technical Processes},\n\tDate-Added = {2012-07-02 19:31:35 +0200},\n\tDate-Modified = {2014-08-27 13:42:11 +0200},\n\tFpage = {714},\n\tGcited = {1},\n\tLpage = {719},\n\tMonth = aug,\n\tNumpages = {3},\n\tPages = {714--719},\n\tPublisher = {Elsevier},\n\tTitle = {Fault Diagnosis of Hybrid Systems: an Onboard Camera Model},\n\tYear = {2012}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Computing the Evolution of Hybrid Systems Using Rigorous Function Calculus.\n \n \n \n\n\n \n Collins, P.; Bresolin, D.; Geretti, L.; and Villa, T.\n\n\n \n\n\n\n In Proc. of the 4th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS12), pages 284–290, Eindhoven, Olanda, June 2012. Elsevier\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
@inproceedings{adhs2012,\n\tAddress = {Eindhoven, Olanda},\n\tAuthor = {P. Collins and D. Bresolin and L. Geretti and T. Villa},\n\tBooktitle = {Proc. of the 4th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS12)},\n\tDate-Added = {2012-07-02 19:26:31 +0200},\n\tDate-Modified = {2014-08-27 13:29:55 +0200},\n\tFpage = {284},\n\tGcited = {5},\n\tLpage = {290},\n\tMonth = jun,\n\tNumpages = {4},\n\tPages = {284--290},\n\tPublisher = {Elsevier},\n\tScited = {1},\n\tTitle = {Computing the Evolution of Hybrid Systems Using Rigorous Function Calculus},\n\tYear = {2012}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n On Begin, Meets and Before.\n \n \n \n\n\n \n Bresolin, D.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n International Journal of Foundations of Computer Science, 23(3): 559–583. 2012.\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
@article{ijfcs2012,\n\tAuthor = {D. Bresolin and P. Sala and G. Sciavicco},\n\tDate-Added = {2011-05-02 19:45:07 +0200},\n\tDate-Modified = {2014-08-27 13:20:56 +0200},\n\tFpage = {559},\n\tGcited = {9},\n\tJournal = {International Journal of Foundations of Computer Science},\n\tLpage = {583},\n\tNumber = {3},\n\tNumpages = {13},\n\tPages = {559--583},\n\tPublisher = {World Scientific Publishing},\n\tScited = {3},\n\tTitle = {On {B}egin, {M}eets and {B}efore},\n\tVolume = {23},\n\tYear = {2012}}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2011\n \n \n (8)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n An Optimal Decision Procedure for MPNL over the Integers.\n \n \n \n\n\n \n Bresolin, D.; Montanari, A.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of GandALF 2011: Second International Symposium on Games, Automata, Logics and Formal Verification, volume 54, of EPTCS, pages 192–206, Minori (Salerno), June 2011. Open Publishing Association\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
@inproceedings{gandalf2011b,\n\tAddress = {Minori (Salerno)},\n\tAuthor = {D. Bresolin and A. Montanari and P. Sala and G. Sciavicco},\n\tBooktitle = {Proc. of GandALF 2011: Second International Symposium on Games, Automata, Logics and Formal Verification},\n\tDate-Added = {2012-07-02 15:37:55 +0200},\n\tDate-Modified = {2014-08-27 13:47:41 +0200},\n\tFpage = {192},\n\tGcited = {3},\n\tLpage = {206},\n\tMonth = jun,\n\tNumpages = {8},\n\tPages = {192--206},\n\tPublisher = {Open Publishing Association},\n\tSeries = {EPTCS},\n\tTitle = {An Optimal Decision Procedure for {MPNL} over the Integers},\n\tVolume = {54},\n\tYear = {2011}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Correct-by-construction code generation from hybrid automata specification.\n \n \n \n\n\n \n Bresolin, D.; Guglielmo, L. D.; Geretti, L.; and Villa, T.\n\n\n \n\n\n\n In Proc. of the 7th International Wireless Communication and Mobile Computing Conference (IWCMC2011), pages 1660–1665, Istanbul, Turchia, July 2011. IEEE Comp. Society Press\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
@inproceedings{cyphy2011,\n\tAddress = {Istanbul, Turchia},\n\tAuthor = {D. Bresolin and L. Di Guglielmo and L. Geretti and T. Villa},\n\tBooktitle = {Proc. of the 7th International Wireless Communication and Mobile Computing Conference (IWCMC2011)},\n\tDate-Added = {2012-01-27 16:14:58 +0100},\n\tDate-Modified = {2014-08-27 13:27:29 +0200},\n\tFpage = {1660},\n\tGcited = {6},\n\tLpage = {1665},\n\tMonth = jul,\n\tNumpages = {3},\n\tPages = {1660--1665},\n\tPublisher = {IEEE Comp. Society Press},\n\tScited = {3},\n\tTitle = {Correct-by-construction code generation from hybrid automata specification},\n\tYear = {2011}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n What's decidable about Halpern and Shoham's interval logic? The maximal fragment ABBL.\n \n \n \n\n\n \n Bresolin, D.; Montanari, A.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of LICS 2011: 26th Symposium on Logic in Computer Science, pages 387–396, Toronto, Canada, June 2011. IEEE Comp. Society Press\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
@inproceedings{lics2011,\n\tAddress = {Toronto, Canada},\n\tAuthor = {D. Bresolin and A. Montanari and P. Sala and G. Sciavicco},\n\tBooktitle = {Proc. of LICS 2011: 26th Symposium on Logic in Computer Science},\n\tDate-Added = {2012-01-27 16:14:58 +0100},\n\tDate-Modified = {2014-08-27 13:03:11 +0200},\n\tFpage = {387},\n\tGcited = {17},\n\tLpage = {396},\n\tMonth = jun,\n\tNumpages = {5},\n\tPages = {387--396},\n\tPublisher = {IEEE Comp. Society Press},\n\tScited = {3},\n\tTitle = {What's decidable about {Halpern and Shoham's} interval logic? {The} maximal fragment {ABBL}},\n\tYear = {2011}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Optimal Tableau Systems for Propositional Neighborhood Logic over All, Dense, and Discrete Linear Orders.\n \n \n \n\n\n \n Bresolin, D.; Montanari, A.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of TABLEAUX 2011: The 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 6793, of LNAI, pages 73–87, Berna, Svizzera, July 2011. Springer\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
@inproceedings{tableaux2011,\n\tAddress = {Berna, Svizzera},\n\tAuthor = {D. Bresolin and A. Montanari and P. Sala and G. Sciavicco},\n\tBooktitle = {Proc. of TABLEAUX 2011: The 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods},\n\tDate-Added = {2012-01-27 16:12:55 +0100},\n\tDate-Modified = {2014-08-27 13:14:59 +0200},\n\tFpage = {73},\n\tGcited = {11},\n\tLpage = {87},\n\tMonth = jul,\n\tNumpages = {8},\n\tPages = {73--87},\n\tPublisher = {Springer},\n\tSeries = {LNAI},\n\tTitle = {Optimal Tableau Systems for Propositional Neighborhood Logic over All, Dense, and Discrete Linear Orders},\n\tVolume = {6793},\n\tYear = {2011}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Game-Theoretic approach to Fault Diagnosis of Hybrid Systems.\n \n \n \n\n\n \n Bresolin, D.; and Capiluppi, M.\n\n\n \n\n\n\n In Proc. of GandALF 2011: Second International Symposium on Games, Automata, Logics and Formal Verification, volume 54, of EPTCS, pages 237–249, Minori (Salerno), June 2011. Open Publishing Association\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
@inproceedings{gandalf2011a,\n\tAddress = {Minori (Salerno)},\n\tAuthor = {D. Bresolin and M. Capiluppi},\n\tBooktitle = {Proc. of GandALF 2011: Second International Symposium on Games, Automata, Logics and Formal Verification},\n\tDate-Added = {2012-01-27 16:11:25 +0100},\n\tDate-Modified = {2014-08-27 13:38:38 +0200},\n\tFpage = {237},\n\tGcited = {2},\n\tLpage = {249},\n\tMonth = jun,\n\tNumpages = {7},\n\tPages = {237--249},\n\tPublisher = {Open Publishing Association},\n\tSeries = {EPTCS},\n\tTitle = {A Game-Theoretic approach to Fault Diagnosis of Hybrid Systems},\n\tVolume = {54},\n\tYear = {2011}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The dark side of Interval Temporal Logic: sharpening the undecidability border.\n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Goranko, V.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n In Combi, C.; Leucker, M.; and Wolter, F., editor(s), Proc. of TIME 2011: 18th International Symposium on Temporal Representation and Reasoning, pages 131–138, Lubecca, Germania, September 2011. IEEE Comp. Society Press\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
@inproceedings{time2011dark,\n\tAddress = {Lubecca, Germania},\n\tAuthor = {D. Bresolin and D. {Della Monica} and V. Goranko and A. Montanari and G. Sciavicco},\n\tBooktitle = {Proc. of TIME 2011: 18th International Symposium on Temporal Representation and Reasoning},\n\tDate-Added = {2011-10-31 12:33:01 +0100},\n\tDate-Modified = {2014-08-27 13:02:04 +0200},\n\tEditor = {Carlo Combi and Martin Leucker and Frank Wolter},\n\tFpage = {131},\n\tGcited = {21},\n\tLpage = {138},\n\tMonth = sep,\n\tNumpages = {4},\n\tPages = {131--138},\n\tPublisher = {IEEE Comp. Society Press},\n\tScited = {5},\n\tTitle = {The dark side of {Interval Temporal Logic}: sharpening the undecidability border},\n\tYear = {2011}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The light side of Interval Temporal Logic: the Bernays-Schönfinkel's fragment of CDT.\n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n In Combi, C.; Leucker, M.; and Wolter, F., editor(s), Proc. of TIME 2011: 18th International Symposium on Temporal Representation and Reasoning, pages 123–130, Lubecca, Germania, September 2011. IEEE Comp. Society Press\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
@inproceedings{time2011light,\n\tAddress = {Lubecca, Germania},\n\tAuthor = {D. Bresolin and D. {Della Monica} and A. Montanari and G. Sciavicco},\n\tBooktitle = {Proc. of TIME 2011: 18th International Symposium on Temporal Representation and Reasoning},\n\tDate-Added = {2011-10-31 12:33:01 +0100},\n\tDate-Modified = {2014-08-27 13:38:18 +0200},\n\tEditor = {Carlo Combi and Martin Leucker and Frank Wolter},\n\tFpage = {123},\n\tGcited = {2},\n\tLpage = {130},\n\tMonth = sep,\n\tNumpages = {4},\n\tPages = {123--130},\n\tPublisher = {IEEE Comp. Society Press},\n\tScited = {1},\n\tTitle = {The light side of {Interval Temporal Logic}: the {Bernays-Sch\\"{o}nfinkel's} fragment of {CDT}},\n\tYear = {2011}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Robotic Surgery: Formal Verification of Plans.\n \n \n \n\n\n \n Muradore, R.; Bresolin, D.; Geretti, L.; Fiorini, P.; and Villa, T.\n\n\n \n\n\n\n IEEE Robotics Automation Magazine, 18(3): 24–32. September 2011.\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\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
@article{ram2011,\n\tAuthor = {Muradore, R. and Bresolin, D. and Geretti, L. and Fiorini, P. and Villa, T.},\n\tDate-Added = {2011-10-31 12:32:28 +0100},\n\tDate-Modified = {2014-08-27 13:11:28 +0200},\n\tDoi = {10.1109/MRA.2011.942112},\n\tFpage = {24},\n\tGcited = {16},\n\tIssn = {1070-9932},\n\tJournal = {IEEE Robotics Automation Magazine},\n\tLpage = {32},\n\tMonth = sep,\n\tNumber = {3},\n\tNumpages = {5},\n\tPages = {24--32},\n\tPublisher = {IEEE Robotics and Automation Society},\n\tScited = {8},\n\tTitle = {Robotic Surgery: Formal Verification of Plans},\n\tVolume = {18},\n\tYear = {2011},\n\tBdsk-Url-1 = {http://dx.doi.org/10.1109/MRA.2011.942112}}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2010\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n A decidable spatial generalization of Metric Interval Temporal Logic.\n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Montanari, A.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of TIME 2010: 17th International Symposium on Temporal Representation and Reasoning, pages 95–102, Parigi, Francia, September 2010. IEEE Comp. Society Press\n \n\n\n\n
\n\n\n\n \n\n \n \n doi\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
@inproceedings{time2010,\n\tAddress = {Parigi, Francia},\n\tAuthor = {D. Bresolin and D. {Della Monica} and A. Montanari and P. Sala and G. Sciavicco},\n\tBooktitle = {Proc. of TIME 2010: 17th International Symposium on Temporal Representation and Reasoning},\n\tDate-Added = {2010-05-24 09:29:41 +0200},\n\tDate-Modified = {2019-04-05 12:59:40 +0000},\n\tDoi = {10.1109/TIME.2010.22},\n\tFpage = 95,\n\tGcited = {6},\n\tLpage = 102,\n\tMonth = sep,\n\tNumpages = 4,\n\tPages = {95--102},\n\tPublisher = {IEEE Comp. Society Press},\n\tTitle = {A decidable spatial generalization of Metric Interval Temporal Logic},\n\tYear = {2010}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Undecidability of the Logic of Overlap Relation over Discrete Linear Orderings.\n \n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Goranko, V.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n Electronic Notes in Theoretical Computer Science, 262: 65 - 81. 2010.\n Proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009)\n\n\n\n
\n\n\n\n \n \n \"UndecidabilityPaper\n  \n \n\n \n \n doi\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{entcs2010,\n\tAuthor = {D. Bresolin and {Della Monica}, D. and V. Goranko and A. Montanari and G. Sciavicco},\n\tDate-Added = {2010-05-10 16:34:31 +0200},\n\tDate-Modified = {2014-08-27 13:21:22 +0200},\n\tDoi = {DOI: 10.1016/j.entcs.2010.04.006},\n\tFpage = 65,\n\tGcited = {9},\n\tIssn = {1571-0661},\n\tJournal = {Electronic Notes in Theoretical Computer Science},\n\tKeywords = {octant tiling problem},\n\tLpage = 81,\n\tNote = {Proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009)},\n\tNumpages = 9,\n\tPages = {65 - 81},\n\tPublisher = {Elsevier},\n\tScited = {3},\n\tTitle = {Undecidability of the Logic of Overlap Relation over Discrete Linear Orderings},\n\tUrl = {http://www.sciencedirect.com/science/article/B75H1-500RR7G-6/2/e291d8bc6537efbf7b3e2884efa5867e},\n\tVolume = {262},\n\tYear = {2010},\n\tBdsk-Url-1 = {http://www.sciencedirect.com/science/article/B75H1-500RR7G-6/2/e291d8bc6537efbf7b3e2884efa5867e},\n\tBdsk-Url-2 = {http://dx.doi.org/10.1016/j.entcs.2010.04.006}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Begin, After, and Later: a maximal decidable Interval Temporal Logic.\n \n \n \n\n\n \n Bresolin, D.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of GandALF 2010: First International Symposium on Games, Automata, Logics and Formal Verification, volume 25, of EPTCS, pages 72–88, Minori (Salerno), June 2010. Open Publishing Association\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
@inproceedings{gandalf2010,\n\tAddress = {Minori (Salerno)},\n\tAuthor = {D. Bresolin and P. Sala and G. Sciavicco},\n\tBooktitle = {Proc. of GandALF 2010: First International Symposium on Games, Automata, Logics and Formal Verification},\n\tDate-Added = {2010-05-05 11:10:43 +0200},\n\tDate-Modified = {2014-08-27 13:30:44 +0200},\n\tFpage = 72,\n\tGcited = {5},\n\tLpage = 88,\n\tMonth = jun,\n\tNumpages = 9,\n\tPages = {72--88},\n\tPublisher = {Open Publishing Association},\n\tSeries = {EPTCS},\n\tTitle = {{Begin, After, and Later}: a maximal decidable {Interval Temporal Logic}},\n\tVolume = {25},\n\tYear = {2010}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Metric Propositional Neighborhood Logics: Expressiveness, Decidability, and Undecidability.\n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Goranko, V.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of ECAI 2010: 19th European Conference on Artificial Intelligence, volume 215, of Frontiers in Artificial Intelligence and Applications, pages 695–700, Lisbona, Portogallo, August 2010. IOS Press\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
@inproceedings{ecai2010,\n\tAddress = {Lisbona, Portogallo},\n\tAuthor = {D. Bresolin and D. {Della Monica} and V. Goranko and A. Montanari and G. Sciavicco},\n\tBooktitle = {Proc. of ECAI 2010: 19th European Conference on Artificial Intelligence},\n\tDate-Added = {2010-04-29 14:17:48 +0200},\n\tDate-Modified = {2014-08-27 13:10:38 +0200},\n\tFpage = 695,\n\tGcited = {17},\n\tLpage = 700,\n\tMonth = aug,\n\tNumpages = 3,\n\tPages = {695--700},\n\tPublisher = {IOS Press},\n\tSeries = {Frontiers in Artificial Intelligence and Applications},\n\tTitle = {Metric Propositional Neighborhood Logics: Expressiveness, Decidability, and Undecidability},\n\tVolume = {215},\n\tYear = {2010}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Tableaux for Logics of Subinterval Structures over Dense Orderings.\n \n \n \n \n\n\n \n Bresolin, D.; Goranko, V.; Montanari, A.; and Sala, P.\n\n\n \n\n\n\n Journal of Logic and Computation, 20(1): 133–166. 2010.\n \n\n\n\n
\n\n\n\n \n \n \"TableauxPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{jlc2010,\n\tAbstract = {In this article, we develop tableau-based decision procedures for the logics of subinterval structures over dense linear orderings. In particular, we consider the two difficult cases: the relation of strict subintervals (with both endpoints strictly inside the current interval) and the relation of proper subintervals (that can share one endpoint with the current interval). For each of these logics, we establish a small pseudo-model property and construct a sound, complete and terminating tableau that searches systematically for existence of such a pseudo-model satisfying the input formulas. Both constructions are non-trivial, but the latter is substantially more complicated because of the presence of beginning and ending subintervals which require special treatment. We prove PSPACE completeness for both procedures and implement them in the generic tableau-based theorem prover Lotrec.\n},\n\tAuthor = {D. Bresolin and V. Goranko and A. Montanari and Sala, P.},\n\tDate-Added = {2009-06-23 18:38:27 +0200},\n\tDate-Modified = {2014-08-27 12:58:04 +0200},\n\tDoi = {10.1093/logcom/exn063},\n\tEprint = {http://logcom.oxfordjournals.org/cgi/reprint/exn063v1.pdf},\n\tFpage = 133,\n\tGcited = {41},\n\tJournal = {Journal of Logic and Computation},\n\tLpage = 166,\n\tNumber = {1},\n\tNumpages = 17,\n\tPages = {133--166},\n\tPublisher = {Oxford University Press},\n\tScited = {12},\n\tTitle = {{Tableaux for Logics of Subinterval Structures over Dense Orderings}},\n\tUrl = {http://logcom.oxfordjournals.org/cgi/content/abstract/exn063v1},\n\tVolume = {20},\n\tYear = {2010},\n\tBdsk-Url-1 = {http://logcom.oxfordjournals.org/cgi/content/abstract/exn063v1},\n\tBdsk-Url-2 = {http://dx.doi.org/10.1093/logcom/exn063}}\n\n
\n
\n\n\n
\n In this article, we develop tableau-based decision procedures for the logics of subinterval structures over dense linear orderings. In particular, we consider the two difficult cases: the relation of strict subintervals (with both endpoints strictly inside the current interval) and the relation of proper subintervals (that can share one endpoint with the current interval). For each of these logics, we establish a small pseudo-model property and construct a sound, complete and terminating tableau that searches systematically for existence of such a pseudo-model satisfying the input formulas. Both constructions are non-trivial, but the latter is substantially more complicated because of the presence of beginning and ending subintervals which require special treatment. We prove PSPACE completeness for both procedures and implement them in the generic tableau-based theorem prover Lotrec. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2009\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Complete and Terminating Tableau for the Logic of Proper Subinterval Structures Over Dense Orderings.\n \n \n \n \n\n\n \n Bresolin, D.; Goranko, V.; Montanari, A.; and Sala, P.\n\n\n \n\n\n\n Electronic Notes in Theoretical Computer Science, 231: 131–151. 2009.\n Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007)\n\n\n\n
\n\n\n\n \n \n \"CompletePaper\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{entcs2009,\n\tAuthor = {D. Bresolin and V. Goranko and A. Montanari and Sala, P.},\n\tDate-Added = {2010-05-10 16:34:31 +0200},\n\tDate-Modified = {2013-07-24 14:44:25 +0200},\n\tDay = {25},\n\tFpage = 131,\n\tGcited = {11},\n\tIsbn = {1571-0661},\n\tJournal = {Electronic Notes in Theoretical Computer Science},\n\tKeywords = {Interval Temporal Logic; Tableau Method; Dense Structure},\n\tLpage = 151,\n\tM3 = {doi: DOI: 10.1016/j.entcs.2009.02.033},\n\tNote = {Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007)},\n\tNumpages = 11,\n\tPages = {131--151},\n\tPublisher = {Elsevier},\n\tTitle = {Complete and Terminating Tableau for the Logic of Proper Subinterval Structures Over Dense Orderings},\n\tTy = {JOUR},\n\tUrl = {http://www.sciencedirect.com/science/article/B75H1-4VWK6J7-9/2/91b78c46f0a844ba3aa669c920f40165},\n\tVolume = {231},\n\tYear = {2009},\n\tBdsk-Url-1 = {http://www.sciencedirect.com/science/article/B75H1-4VWK6J7-9/2/91b78c46f0a844ba3aa669c920f40165}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths.\n \n \n \n\n\n \n Bresolin, D.; Goranko, V.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM), pages 240–249, Hanoi, Vietnam, November 2009. IEEE Comp. Society Press\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
@inproceedings{sefm2009,\n\tAddress = {Hanoi, Vietnam},\n\tAuthor = {D. Bresolin and V. Goranko and A. Montanari and G. Sciavicco},\n\tBooktitle = {Proc. of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM)},\n\tDate-Added = {2009-11-03 16:26:15 +0100},\n\tDate-Modified = {2014-08-27 13:00:13 +0200},\n\tFpage = 240,\n\tGcited = {18},\n\tLpage = 249,\n\tMonth = nov,\n\tNumpages = 5,\n\tPages = {240--249},\n\tPublisher = {IEEE Comp. Society Press},\n\tScited = {10},\n\tTitle = {Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths},\n\tYear = {2009}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Propositional Interval Neighborhood Logics: Expressiveness, Decidability, and Undecidable Extensions.\n \n \n \n\n\n \n Bresolin, D.; Goranko, V.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n Annals of Pure and Applied Logic, 161: 289–304. 2009.\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
@article{apal2009,\n\tAuthor = {D. Bresolin and V. Goranko and A. Montanari and G. Sciavicco},\n\tDate-Added = {2009-06-23 18:36:38 +0200},\n\tDate-Modified = {2014-08-27 12:55:43 +0200},\n\tFpage = 289,\n\tGcited = {60},\n\tJournal = {Annals of Pure and Applied Logic},\n\tLpage = 304,\n\tNumpages = 8,\n\tPages = {289--304},\n\tPublisher = {Elsevier},\n\tScited = {33},\n\tTitle = {Propositional Interval Neighborhood Logics: Expressiveness, Decidability, and Undecidable Extensions},\n\tVolume = {161},\n\tYear = {2009}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n The impact of EFSM Composition on Functional ATPG.\n \n \n \n\n\n \n Bresolin, D.; Di Guglielmo, G.; Fummi, F.; Pravadelli, G.; and Villa, T.\n\n\n \n\n\n\n In Proc. of the 12th IEEE Symposium on Design and Diagnostics of Electronic Systems (DDECS09), pages 44–49, Liberec, Repubblica Ceca, April 2009. IEEE Comp. Society Press\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
@inproceedings{ddecs2009,\n\tAddress = {Liberec, Repubblica Ceca},\n\tAuthor = {D. Bresolin and G. {Di Guglielmo} and F. Fummi and G. Pravadelli and T. Villa},\n\tBooktitle = {Proc. of the 12th IEEE Symposium on Design and Diagnostics of Electronic Systems (DDECS09)},\n\tDate-Added = {2009-06-23 18:36:23 +0200},\n\tDate-Modified = {2014-08-27 13:40:18 +0200},\n\tFpage = 44,\n\tGcited = {2},\n\tLpage = 49,\n\tMonth = apr,\n\tNumpages = 3,\n\tPages = {44--49},\n\tPublisher = {IEEE Comp. Society Press},\n\tScited = {1},\n\tTitle = {The impact of {EFSM} Composition on Functional {ATPG}},\n\tYear = {2009}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n On the Undecidability of Interval Temporal Logics with the Overlap Modality.\n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Goranko, V.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of TIME 2009: 16th International Symposium on Temporal Representation and Reasoning, pages 88–95, Brixen-Bressanone, Italia, July 2009. IEEE Comp. Society Press\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
@inproceedings{time2009,\n\tAddress = {Brixen-Bressanone, Italia},\n\tAuthor = {D. Bresolin and D. {Della Monica} and V. Goranko and A. Montanari and G. Sciavicco},\n\tBooktitle = {Proc. of TIME 2009: 16th International Symposium on Temporal Representation and Reasoning},\n\tDate-Added = {2009-06-23 18:36:18 +0200},\n\tDate-Modified = {2014-08-27 13:12:47 +0200},\n\tFpage = 88,\n\tGcited = {13},\n\tLpage = 95,\n\tMonth = jul,\n\tNumpages = 4,\n\tPages = {88--95},\n\tPublisher = {IEEE Comp. Society Press},\n\tScited = {9},\n\tTitle = {On the Undecidability of Interval Temporal Logics with the Overlap Modality},\n\tYear = {2009}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A Tableau-Based System for Spatial Reasoning about Directional Relations.\n \n \n \n\n\n \n Bresolin, D.; Montanari, A.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of TABLEAUX 2009: 18th Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 5607, of LNAI, pages 123–137, Oslo, Norvegia, July 2009. Springer\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
@inproceedings{tableaux2009,\n\tAddress = {Oslo, Norvegia},\n\tAuthor = {D. Bresolin and A. Montanari and P. Sala and G. Sciavicco},\n\tBooktitle = {Proc. of TABLEAUX 2009: 18th Conference on Automated Reasoning with Analytic Tableaux and Related Methods},\n\tDate-Added = {2009-06-23 18:36:03 +0200},\n\tDate-Modified = {2013-07-24 14:44:25 +0200},\n\tFpage = 123,\n\tGcited = {8},\n\tLpage = 137,\n\tMonth = jul,\n\tNumpages = 8,\n\tPages = {123--137},\n\tPublisher = {Springer},\n\tScited = {1},\n\tSeries = {LNAI},\n\tTitle = {A Tableau-Based System for Spatial Reasoning about Directional Relations},\n\tVolume = {5607},\n\tYear = {2009}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A theory of ultimately periodic languages and automata with an application to time granularity.\n \n \n \n \n\n\n \n Bresolin, D.; Montanari, A.; and Puppis, G.\n\n\n \n\n\n\n Acta Informatica, 46(5): 331–360. March 2009.\n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{acta2009,\n\tAbstract = {Abstract~~In this paper, we develop a theory of regular {\\oe}{\\^a}-languages that consist of ultimately periodic words only and we provide it with an automaton-based characterization. The resulting class of automata, called ultimately periodic automata (UPA), is a subclass of the class of Büchi automata and inherits some properties of automata over finite words (NFA). Taking advantage of the similarities among UPA, Büchi automata, and NFA, we devise efficient solutions to a number of basic problems for UPA, such as the inclusion, the equivalence, and the size optimization problems. The original motivation for developing a theory of ultimately periodic languages and automata was to represent and to reason about sets of time granularities in knowledge-based and database systems. In the last part of the paper, we show that UPA actually allow one to represent (possibly infinite) sets of granularities, instead of single ones, in a compact and suitable to algorithmic manipulation way. In particular, we describe an application of UPA to a concrete time granularity scenario taken from clinical medicine. },\n\tAuthor = {D. Bresolin and A. Montanari and G. Puppis},\n\tDate-Added = {2009-06-23 18:21:53 +0200},\n\tDate-Modified = {2013-07-24 14:37:30 +0200},\n\tDoi = {10.1007/s00236-009-0094-7},\n\tFpage = 331,\n\tGcited = {2},\n\tJournal = {Acta Informatica},\n\tLpage = 360,\n\tMonth = mar,\n\tNumber = {5},\n\tNumpages = 15,\n\tPages = {331--360},\n\tPublisher = {Springer},\n\tScited = {1},\n\tTitle = {A theory of ultimately periodic languages and automata with an application to time granularity},\n\tUrl = {http://dx.doi.org/10.1007/s00236-009-0094-7},\n\tVolume = {46},\n\tYear = {2009},\n\tBdsk-Url-1 = {http://dx.doi.org/10.1007/s00236-009-0094-7}}\n\n
\n
\n\n\n
\n Abstract~~In this paper, we develop a theory of regular ω-languages that consist of ultimately periodic words only and we provide it with an automaton-based characterization. The resulting class of automata, called ultimately periodic automata (UPA), is a subclass of the class of Büchi automata and inherits some properties of automata over finite words (NFA). Taking advantage of the similarities among UPA, Büchi automata, and NFA, we devise efficient solutions to a number of basic problems for UPA, such as the inclusion, the equivalence, and the size optimization problems. The original motivation for developing a theory of ultimately periodic languages and automata was to represent and to reason about sets of time granularities in knowledge-based and database systems. In the last part of the paper, we show that UPA actually allow one to represent (possibly infinite) sets of granularities, instead of single ones, in a compact and suitable to algorithmic manipulation way. In particular, we describe an application of UPA to a concrete time granularity scenario taken from clinical medicine. \n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2008\n \n \n (4)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification.\n \n \n \n\n\n \n Bresolin, D.; Della Monica, D.; Goranko, V.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of the 15th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008), volume 5330, of LNCS, pages 590–604, Doha, Quatar, November 2008. Springer\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 abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{lpar2008,\n\tAbstract = {Interval temporal logics are based on temporal structures where time intervals, rather than time instants, are the primitive ontological entities. They employ modal operators corresponding to various relations between intervals, known as Allen‚{\\"A}{\\^o}s relations. Technically, validity in interval temporal logics translates to dyadic second-order logic, thus explaining their complex computational behavior. The full modal logic of Allen‚{\\"A}{\\^o}s relations, called HS, has been proved to be undecidable by Halpern and Shoham under very weak assumptions on the class of interval structures, and this result was discouraging attempts for practical applications and further research in the field. A renewed interest has been recently stimulated by the discovery of interesting decidable fragments of HS. This paper contributes to the characterization of the boundary between decidability and undecidability of HS fragments. It summarizes known positive and negative results, it describes the main techniques applied so far in both directions, and it establishes a number of new undecidability results for relatively small fragments of HS. },\n\tAddress = {Doha, Quatar},\n\tAuthor = {D. Bresolin and {Della Monica}, D. and V. Goranko and A. Montanari and Sciavicco, G.},\n\tBooktitle = {Proc. of the 15th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008)},\n\tDate-Added = {2009-06-26 12:46:16 +0200},\n\tDate-Modified = {2014-08-27 12:57:14 +0200},\n\tFpage = 590,\n\tGcited = {45},\n\tLpage = 604,\n\tMonth = nov,\n\tNumpages = 8,\n\tPages = {590--604},\n\tPublisher = {Springer},\n\tScited = {10},\n\tSeries = {LNCS},\n\tTitle = {Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification},\n\tVolume = {5330},\n\tYear = {2008},\n\tBdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-89439-1_41}}\n\n
\n
\n\n\n
\n Interval temporal logics are based on temporal structures where time intervals, rather than time instants, are the primitive ontological entities. They employ modal operators corresponding to various relations between intervals, known as Allen’s relations. Technically, validity in interval temporal logics translates to dyadic second-order logic, thus explaining their complex computational behavior. The full modal logic of Allen’s relations, called HS, has been proved to be undecidable by Halpern and Shoham under very weak assumptions on the class of interval structures, and this result was discouraging attempts for practical applications and further research in the field. A renewed interest has been recently stimulated by the discovery of interesting decidable fragments of HS. This paper contributes to the characterization of the boundary between decidability and undecidability of HS fragments. It summarizes known positive and negative results, it describes the main techniques applied so far in both directions, and it establishes a number of new undecidability results for relatively small fragments of HS. \n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Optimal tableaux for Right Propositional Neighborhood Logic over Linear Orders.\n \n \n \n\n\n \n Bresolin, D.; Montanari, A.; Sala, P.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of JELIA 2008: 11th European Conference on Logics in Artificial Intelligence (JELIA), volume 5293, of LNAI, pages 62–75, Dresda, Germania, September 2008. Springer\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
@inproceedings{jelia2008,\n\tAddress = {Dresda, Germania},\n\tAuthor = {D. Bresolin and A. Montanari and P. Sala and G. Sciavicco},\n\tBooktitle = {Proc. of JELIA 2008: 11th European Conference on Logics in Artificial Intelligence (JELIA)},\n\tDate-Added = {2009-06-23 18:35:33 +0200},\n\tDate-Modified = {2014-08-27 12:58:39 +0200},\n\tFpage = 62,\n\tGcited = {27},\n\tLpage = 75,\n\tMonth = sep,\n\tNumpages = 7,\n\tPages = {62--75},\n\tPublisher = {Springer},\n\tScited = {4},\n\tSeries = {LNAI},\n\tTitle = {Optimal tableaux for Right Propositional Neighborhood Logic over Linear Orders},\n\tVolume = {5293},\n\tYear = {2008}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An optimal tableau for Right Propositional Neighborhood Logic over trees.\n \n \n \n\n\n \n Bresolin, D.; Montanari, A.; and Sala, P.\n\n\n \n\n\n\n In Proc. of the 15th International Symposium on Temporal Representation and Reasoning (TIME 2008), pages 110–117, Montreal, Quebec, Canada, June 2008. IEEE Comp. Society Press\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
@inproceedings{time2008,\n\tAddress = {Montreal, Quebec, Canada},\n\tAuthor = {D. Bresolin and A. Montanari and P. Sala},\n\tBooktitle = {Proc. of the 15th International Symposium on Temporal Representation and Reasoning (TIME 2008)},\n\tDate-Added = {2008-03-12 14:20:25 +0100},\n\tDate-Modified = {2013-07-24 14:44:25 +0200},\n\tFpage = 110,\n\tGcited = {2},\n\tLpage = 117,\n\tMonth = jun,\n\tNumpages = 4,\n\tPages = {110--117},\n\tPublisher = {IEEE Comp. Society Press},\n\tScited = {1},\n\tTitle = {An optimal tableau for {R}ight {P}ropositional {N}eighborhood {L}ogic over trees},\n\tYear = {2008}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Reachability computation for hybrid systems with Ariadne.\n \n \n \n\n\n \n Benvenuti, L.; Bresolin, D.; Casagrande, A.; Collins, P.; Ferrari, A.; Mazzi, E.; Sangiovanni-Vincentelli, A.; and Villa, T.\n\n\n \n\n\n\n In Proc. of the 17th IFAC World Congress, pages 8960–8965, Seul, Corea del Sud, July 2008. Elsevier\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
@inproceedings{ifac2008,\n\tAddress = {Seul, Corea del Sud},\n\tAuthor = {L. Benvenuti and D. Bresolin and A. Casagrande and P. Collins and A. Ferrari and E. Mazzi and A. Sangiovanni-Vincentelli and T. Villa},\n\tBooktitle = {Proc. of the 17th IFAC World Congress},\n\tDate-Added = {2007-12-10 12:50:08 +0100},\n\tDate-Modified = {2014-08-27 13:02:32 +0200},\n\tFpage = 8960,\n\tGcited = {19},\n\tLpage = 8965,\n\tMonth = jul,\n\tNumpages = 3,\n\tPages = {8960--8965},\n\tPublisher = {Elsevier},\n\tTitle = {Reachability computation for hybrid systems with {Ariadne}},\n\tYear = {2008}}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2007\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Proof methods for Interval Temporal Logics.\n \n \n \n\n\n \n Bresolin, D.\n\n\n \n\n\n\n Ph.D. Thesis, Dipartimento di Matematica e Informatica, Università degli Studi di Udine, 2007.\n Forum Editrice, PhD Thesis Series CS 2007\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
@phdthesis{phdthesis,\n\tAddress = {Universit\\`a degli Studi di Udine},\n\tAuthor = {D. Bresolin},\n\tDate-Added = {2007-05-04 13:01:13 +0200},\n\tDate-Modified = {2014-08-27 13:35:20 +0200},\n\tGcited = {3},\n\tNote = {Forum Editrice, PhD Thesis Series CS 2007},\n\tNumpages = 33,\n\tPublisher = {Forum Editrice},\n\tSchool = {Dipartimento di Matematica e Informatica},\n\tTitle = {Proof methods for {Interval Temporal Logics}},\n\tYear = {2007}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Tableau Systems for Logics of Subinterval Structures over Dense Orderings.\n \n \n \n\n\n \n Bresolin, D.; Goranko, V.; Montanari, A.; and Sala, P.\n\n\n \n\n\n\n In Proc. of TABLEAUX 2007: 16th Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 4548, of LNAI, pages 73–89, Aix en Provence, Francia, July 2007. Springer\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
@inproceedings{tableaux2007,\n\tAddress = {Aix en Provence, Francia},\n\tAuthor = {D. Bresolin and V. Goranko and A. Montanari and P. Sala},\n\tBooktitle = {Proc. of TABLEAUX 2007: 16th Conference on Automated Reasoning with Analytic Tableaux and Related Methods},\n\tDate-Added = {2007-05-04 10:24:50 +0200},\n\tDate-Modified = {2014-08-27 13:00:42 +0200},\n\tFpage = 73,\n\tGcited = {14},\n\tLpage = 89,\n\tMonth = jul,\n\tNumpages = 9,\n\tPages = {73--89},\n\tPublisher = {Springer},\n\tScited = {9},\n\tSeries = {LNAI},\n\tTitle = {Tableau Systems for Logics of Subinterval Structures over Dense Orderings},\n\tVolume = {4548},\n\tYear = {2007}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n On Decidability and Expressiveness of Propositional Interval Neighborhood Logics.\n \n \n \n\n\n \n Bresolin, D.; Goranko, V.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n In Proc. of LFCS 2007: Symposium on Logical Foundations of Computer Science, volume 4514, of LNCS, pages 84–99, New York, USA, June 2007. Springer\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
@inproceedings{lfcs07,\n\tAddress = {New York, USA},\n\tAuthor = {D. Bresolin and V. Goranko and A. Montanari and G. Sciavicco},\n\tBooktitle = {Proc. of LFCS 2007: Symposium on Logical Foundations of Computer Science},\n\tDate-Added = {2007-03-07 17:12:18 +0100},\n\tDate-Modified = {2014-08-27 12:56:42 +0200},\n\tFpage = 84,\n\tGcited = {34},\n\tLpage = 99,\n\tMonth = jun,\n\tNumpages = 8,\n\tPages = {84--99},\n\tPublisher = {Springer},\n\tScited = {11},\n\tSeries = {LNCS},\n\tTitle = {On Decidability and Expressiveness of Propositional Interval Neighborhood Logics},\n\tVolume = {4514},\n\tYear = {2007}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An optimal tableau-based decision algorithm for Propositional Neighborhood Logic.\n \n \n \n\n\n \n Bresolin, D.; Montanari, A.; and Sala, P.\n\n\n \n\n\n\n In Proc. of STACS 2007: 24th International Symposium on Theoretical Aspects of Computer Science, volume 4393, of LNCS, pages 549–560, Aachen, Germania, February 2007. Springer\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
@inproceedings{stacs07,\n\tAddress = {Aachen, Germania},\n\tAuthor = {D. Bresolin and A. Montanari and P. Sala},\n\tBooktitle = {Proc. of STACS 2007: 24th International Symposium on Theoretical Aspects of Computer Science},\n\tDate-Modified = {2014-08-27 12:56:10 +0200},\n\tFpage = 549,\n\tGcited = {38},\n\tLpage = 560,\n\tMonth = feb,\n\tNumpages = 6,\n\tPages = {549--560},\n\tPublisher = {Springer},\n\tScited = {18},\n\tSeries = {LNCS},\n\tTitle = {An optimal tableau-based decision algorithm for Propositional Neighborhood Logic},\n\tVolume = {4393},\n\tYear = {2007}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n An optimal decision procedure for Right Propositional Neighborhood Logic.\n \n \n \n\n\n \n Bresolin, D.; Montanari, A.; and Sciavicco, G.\n\n\n \n\n\n\n Journal of Automated Reasoning, 38(1-3): 173–199. 2007.\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
@article{jar2007,\n\tAuthor = {D. Bresolin and A. Montanari and G. Sciavicco},\n\tDate-Modified = {2014-08-27 12:55:21 +0200},\n\tFpage = 173,\n\tGcited = {52},\n\tJournal = {Journal of Automated Reasoning},\n\tLpage = 199,\n\tNumber = {1-3},\n\tNumpages = 14,\n\tPages = {173--199},\n\tPublisher = {Springer},\n\tScited = {26},\n\tTitle = {An optimal decision procedure for Right Propositional Neighborhood Logic},\n\tVolume = {38},\n\tYear = {2007}}\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2006\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Relational dual tableaux for interval temporal logics.\n \n \n \n\n\n \n Bresolin, D.; Golińska-Pilarek, J.; and Orłowska, E.\n\n\n \n\n\n\n Journal of Applied Non-Classical Logics, 16(3–4): 251–277. 2006.\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
@article{jancl06,\n\tAuthor = {D. Bresolin and J. Goli\\'{n}ska-Pilarek and E. Or{\\l}owska},\n\tDate-Modified = {2014-08-27 13:31:32 +0200},\n\tFpage = 251,\n\tGcited = {5},\n\tJournal = {Journal of Applied Non-Classical Logics},\n\tLpage = 277,\n\tNumber = {3--4},\n\tNumpages = 14,\n\tPages = {251--277},\n\tPublisher = {Lavoisier},\n\tScited = {3},\n\tTitle = {Relational dual tableaux for interval temporal logics},\n\tVolume = {16},\n\tYear = {2006}}\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 A tableau-based decision procedure for a branching-time interval temporal logic.\n \n \n \n\n\n \n Bresolin, D.; and Montanari, A.\n\n\n \n\n\n\n In Schlingloff, H., editor(s), Proc. of M4M-4: 4th International Workshop on Methods for Modalities, Berlino, Germania, December 2005. Humboldt University\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
@inproceedings{m4m2005,\n\tAddress = {Berlino, Germania},\n\tAuthor = {D. Bresolin and A. Montanari},\n\tBooktitle = {Proc. of M4M-4: 4th International Workshop on Methods for Modalities},\n\tDate-Added = {2009-11-03 16:24:15 +0100},\n\tDate-Modified = {2013-07-24 14:36:52 +0200},\n\tEditor = {H. Schlingloff},\n\tGcited = {9},\n\tMonth = dec,\n\tNumpages = 8,\n\tPublisher = {Humboldt University},\n\tTitle = {A tableau-based decision procedure for a branching-time interval temporal logic},\n\tYear = {2005}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n A tableau-based decision procedure for Right Propositional Neighborhood Logic.\n \n \n \n\n\n \n Bresolin, D.; and Montanari, A.\n\n\n \n\n\n\n In Proc. of TABLEAUX 2005: 14th Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 3702, of Lecture Notes in Artificial Intelligence, pages 63–77, Koblenz, Germania, September 2005. Springer\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
@inproceedings{tableaux2005,\n\tAddress = {Koblenz, Germania},\n\tAuthor = {D. Bresolin and A. Montanari},\n\tBooktitle = {Proc. of TABLEAUX 2005: 14th Conference on Automated Reasoning with Analytic Tableaux and Related Methods},\n\tDate-Modified = {2014-08-27 12:59:04 +0200},\n\tFpage = 63,\n\tGcited = {21},\n\tLpage = 77,\n\tMonth = sep,\n\tNumpages = 8,\n\tPages = {63--77},\n\tPublisher = {Springer},\n\tScited = {9},\n\tSeries = {Lecture Notes in Artificial Intelligence},\n\tTitle = {A tableau-based decision procedure for Right Propositional Neighborhood Logic},\n\tVolume = {3702},\n\tYear = {2005}}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2004\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Time Granularities and Ultimately Periodic Automata.\n \n \n \n\n\n \n Bresolin, D.; Montanari, A.; and Puppis, G.\n\n\n \n\n\n\n In Proc. of JELIA 2004: 9th European Conference on Logics in Artificial Intelligence, volume 3229, of Lecture Notes in Artificial Intelligence, pages 513–525, Lisbona, Portogallo, September 2004. Springer\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
@inproceedings{jelia2004,\n\tAddress = {Lisbona, Portogallo},\n\tAuthor = {D. Bresolin and A. Montanari and G. Puppis},\n\tBooktitle = {Proc. of JELIA 2004: 9th European Conference on Logics in Artificial Intelligence},\n\tDate-Modified = {2014-08-27 12:59:29 +0200},\n\tFpage = 513,\n\tGcited = {21},\n\tLpage = 525,\n\tMonth = sep,\n\tNumpages = 7,\n\tPages = {513--525},\n\tPublisher = {Springer},\n\tScited = {7},\n\tSeries = {Lecture Notes in Artificial Intelligence},\n\tTitle = {Time Granularities and Ultimately Periodic Automata},\n\tVolume = {3229},\n\tYear = {2004}}\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);