The CAP Sino-German Project
2020
Conformance-Based Doping Detection for Cyber-Physical Systems Dimitrova, R.; Gazda, M.; Mousavi, M. R.; Biewer, S. and Hermanns, H.
In Formal Techniques for Distributed Objects, Components, and Systems
- 40th IFIP WG 6.1 International Conference, FORTE 2020, Held
as Part of the 15th International Federated Conference on Distributed
Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19,
2020, Proceedings , pages 59-77, Springer Connection models for the Internet-of-Things He, K.; Hermanns, H.; Wu, H. and Chen, Y.
In Frontiers Comput. Sci. , 14: 143401, 2020.Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions Winterer, L.; Junges, S.; Wimmer, R.; Jansen, N.; Topcu, U.; Katoen, J.-P. and Becker, B.
In IEEE Transactions on Automatic Control : 1-1, 2020.
2019
The 10, 000 Facets of MDP Model Checking Baier, C.; Hermanns, H. and Katoen, J.-P.
In Computing and Software Science - State of the Art and Perspectives , pages 420-451, Springer Doping Tests for Cyber-Physical Systems Biewer, S.; D'Argenio, P. R. and Hermanns, H.
In Quantitative Evaluation of Systems, 16th International Conference,
QEST 2019, Glasgow, UK, September 10-12, 2019, Proceedings , pages 313-331, Springer Battery-aware scheduling in low orbit: the GomX-3 case Bisgaard, M.; Gerhardt, D.; Hermanns, H.; Krcál, J.; Nies, G. and Stenger, M.
In Formal Aspects Comput. , 31: 261-285, 2019.ROLL 1.0: ω-Regular Language Learning Library Li, Y.; Sun, X.; Turrini, A.; Chen, Y.-F. and Xu, J.
In TACAS , pages 365-371, LNCS 11427, 2019.Interval Markov Decision Processes with Multiple Objectives: from Robust Strategies to Pareto Curves Hahn, E. M.; Hashemi, V.; Hermanns, H.; Lahijanian, M. and Turrini, A.
In TOMACS , 2019.On the hardness of analyzing probabilistic programs Kaminski, B. L.; Katoen, J.-P. and Matheja, C.
In Acta Informatica , 56: 255-285, 2019.
2018
Cyber-Physical Doping Tests Biewer, S.; D'Argenio, P. R. and Hermanns, H.
In 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems,
MT@CPSWeek 2018, Porto, Portugal, April 10, 2018 , pages 18-19, IEEE Markov Automata on Discount! Butkova, Y.; Wimmer, R. and Hermanns, H.
In Measurement, Modelling and Evaluation of Computing Systems - 19th
International GI/ITG Conference, MMB 2018, Erlangen, Germany,
February 26-28, 2018, Proceedings , pages 19-34, Springer Advanced Automata-based Algorithms for Program Termination Checking Chen, Y.-F.; Heizmann, M.; Lengál, O.; Li, Y.; Tsai, M.-H.; Turrini, A. and Zhang, L.
In PLDI , 2018.Synthesis in pMDPs: A Tale of 1001 Parameters Cubuktepe, M.; Jansen, N.; Junges, S.; Katoen, J.-P. and Topcu, U.
In ATVA , pages 160-176, Springer , Lecture Notes in Computer Science 11138, 2018.The Quest for Minimal Quotients for Probabilistic and Markov Automata Eisentraut, C.; Hermanns, H.; Schuster, J.; Turrini, A. and Zhang, L.
In Information and Computation , 262, Part 1: 162-186, 2018.Monitoring CTMCs by Multi-clock Timed Automata Feng, Y.; Katoen, J.-P.; Li, H.; Xia, B. and Zhan, N.
In CAV (1) , pages 507-526, Springer , Lecture Notes in Computer Science 10981, 2018.Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent
Systems Fu, C.; Turrini, A.; Huang, X.; Song, L.; Feng, Y. and Zhang, L.
In Proceedings of the Twenty-Seventh International Joint Conference on
Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm,
Sweden , pages 4757-4763, ijcai.org Multi-cost Bounded Reachability in MDP Hartmanns, A.; Junges, S.; Katoen, J.-P. and Quatmann, T.
In TACAS (2) , pages 320-339, Springer , Lecture Notes in Computer Science 10806, 2018.Verification, Testing, and Runtime Monitoring of Automotive Exhaust
Emissions Hermanns, H.; Biewer, S.; D'Argenio, P. R. and Köhl, M. A.
In LPAR-22. 22nd International Conference on Logic for Programming,
Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November
2018 , pages 1-17, EasyChair , EPiC Series in Computing 57, 2018.One Net Fits All - A Unifying Semantics of Dynamic
Fault Trees Using
GSPNs Junges, S.; Katoen, J.-P.; Stoelinga, M. and Volk, M.
In Petri Nets , pages 272-293, Springer , Lecture Notes in Computer Science 10877, 2018.Model Checking for Safe Navigation Among Humans Junges, S.; Jansen, N.; Katoen, J.-P.; Topcu, U.; Zhang, R. and Hayhoe, M. M.
In QEST , pages 207-222, Springer , Lecture Notes in Computer Science 11024, 2018.Learning to Complement Büchi Automata Li, Y.; Turrini, A.; Zhang, L. and Schewe, S.
In VMCAI , pages 313-335, LNCS 10747, 2018.Mastering operational limitations of LEO satellites – The GomX-3 approach Nies, G.; Stenger, M.; Krčál, J.; Hermanns, H.; Bisgaard, M.; Gerhardt, D.; Haverkort, B.; Jongerden, M.; Larsen, K. G. and Wognsen, E. R.
In Acta Astronautica , 151: 726-735, 2018.Conditioning in Probabilistic Programming Olmedo, F.; Gretz, F.; Jansen, N.; Kaminski, B. L.; Katoen, J.-P. and McIver, A.
In ACM Trans. Program. Lang. Syst. , 40: 4:1-4:50, 2018.Sound Value Iteration Quatmann, T. and Katoen, J.-P.
In CAV (1) , pages 643-661, Springer , Lecture Notes in Computer Science 10981, 2018.Branching Bisimulation and Concurrent Object Verification Yang, X.; Katoen, J.-P.; Lin, H.; Liu, G. and Wu, H.
In DSN , pages 267-278, IEEE Computer Society , 2018.Probabilistic Bisimulation for Realistic Schedulers Zhang, L.; Yang, P.; Song, L.; Hermanns, H.; Eisentraut, C.; Jansen, D. N. and Godskesen, J. C.
In Acta Inf. , 2018.
2017
Teaching Academic Concurrency to Amazing Students Biewer, S.; Freiberger, F.; Held, P. L. and Hermanns, H.
In Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand
Larsen on the Occasion of His 60th Birthday , pages 170-195, Springer JANI: Quantitative Model and Tool Interaction Budde, C. E.; Dehnert, C.; Hahn, E. M.; Hartmanns, A.; Junges, S. and Turrini, A.
In TACAS , pages 151-168, LNCS 10206, 2017.Long-Run Rewards for Markov Automata Butkova, Y.; Wimmer, R. and Hermanns, H.
In TACAS , pages 188-203, LNCS 10206, 2017.MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems Chen, M.; Han, X.; Tang, T.; Wang, S.; Yang, M.; Zhan, N.; Zhao, H. and Zou, L.
In Provably Correct Systems , pages 38-57, NASA Monographs in Systems and Software Engineering , 2017.Sequential Convex Programming for the Efficient Verification of Parametric MDPs Cubuktepe, M.; Jansen, N.; Junges, S.; Katoen, J.-P.; Papusha, I. and Topcu, U.
In TACAS , pages 133-150, LNCS 10206, 2017.Barrier certificates revisited Dai, L.; Gan, T.; Xia, B. and Zhan, N.
In J. Symb. Comput. , 80: 62-86, 2017.Is Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs D'Argenio, P. R.; Barthe, G.; Biewer, S.; Finkbeiner, B. and Hermanns, H.
In ESOP , pages 83-110, LNCS 10201, 2017.Model Checking ω-regular Properties for Quantum Markov Chains Feng, Y.; Hahn, E. M.; Turrini, A. and Ying, S.
In CONCUR , pages 35:1-35:16, LIPIcs 85, 2017.Precisely deciding CSL formulas through approximate model checking
for CTMCs Feng, Y. and Zhang, L.
In J. Comput. Syst. Sci. , 89: 361-371, 2017.Finding polynomial loop invariants for probabilistic programs Feng, Y.; Zhang, L.; Jansen, D. N.; Zhan, N. and Xia, B.
In ATVA , pages 400-416, LNCS 10482, 2017.On Equivalence Checking of Nondeterministic Finite Automata Fu, C.; Deng, Y.; Jansen, D. N. and Zhang, L.
In Dependable Software Engineering. Theories, Tools, and Applications
- Third International Symposium, SETTA 2017, Changsha, China, October
23-25, 2017, Proceedings , pages 216-231, Springer Model-Based Testing for Asynchronous Systems Graf-Brill, A. and Hermanns, H.
In Critical Systems: Formal Methods and Automated Verification - Joint
22nd International Workshop on Formal Methods for Industrial Critical
Systems - and - 17th International Workshop on Automated Verification
of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18-20,
2017, Proceedings , pages 66-82, Springer Modelling and certification for electric mobility Graf-Brill, A.; Hartmanns, A.; Hermanns, H. and Rose, S.
In 15th IEEE International Conference on Industrial Informatics, INDIN
2017, Emden, Germany, July 24-26, 2017 , pages 109-114, IEEE Multi-objective Robust Strategy Synthesis for Interval MDPs Hahn, E. M.; Hashemi, V.; Hermanns, H.; Lahijanian, M. and Turrini, A.
In QEST , pages 207-223, LNCS 10503, 2017.Synthesising Strategy Improvement and Recursive Algorithms for Solving
2.5 Player Parity Games Hahn, E. M.; Schewe, S.; Turrini, A. and Zhang, L.
In Verification, Model Checking, and Abstract Interpretation - 18th International
Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings , pages 266-287, Springer Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs Hashemi, V.; Turrini, A.; Hahn, E. M.; Hermanns, H. and Elbassioni, K.
In SETTA , pages 25-41, LNCS 10606, 2017. (Best paper award)Cost vs. time in stochastic games and Markov automata Hatefi, H.; Wimmer, R.; Braitling, B.; Fioriti, L. M. F.; Becker, B. and Hermanns, H.
In Formal Aspects Comput. , 29: 629-649, 2017.Models of Connected Things: On Priced Probabilistic Timed Reo He, K.; Hermanns, H. and Chen, Y.
In 41st IEEE Annual Computer Software and Applications Conference,
COMPSAC 2017, Turin, Italy, July 4-8, 2017. Volume 1 , pages 234-243, IEEE Computer Society Fault trees on a diet: automated reduction by graph rewriting Junges, S.; Guck, D.; Katoen, J.-P.; Rensink, A. and Stoelinga, M.
In Formal Asp. Comput. , 29: 651-703, 2017.A weakest pre-expectation semantics for mixed-sign
expectations Kaminski, B. L. and Katoen, J.-P.
In LICS , pages 1-12, IEEE Computer Society , 2017.Modal Stochastic Games - Abstraction-Refinement of
Probabilistic Automata Katoen, J.-P. and Sher, F.
In Models, Algorithms, Logics and Tools , pages 426-445, Springer , Lecture Notes in Computer Science 10460, 2017.A Novel Learning Algorithm for Büchi Automata based on Family of DFAs and Classification Trees Li, Y.; Chen, Y.-F.; Zhang, L. and Liu, D.
In TACAS , pages 208-226, LNCS 10205, 2017.Markov Automata with Multiple Objectives Quatmann, T.; Junges, S. and Katoen, J.-P.
In CAV , pages 140-159, LNCS 10426, 2017.A Formal Design Model of Cloud Services Sun, M. and Fu, G.
In SEKE , pages 173-178, 2017.Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems Wang, Q.; Li, Y.; Xia, B. and Zhan, N.
In J. Systems Science & Complexity , 30: 234-252, 2017.A Compositional Modelling and Verification Framework for Stochastic
Hybrid Systems Wang, S.; Zhan, N. and Zhang, L.
In Formal Asp. Comput. , 29: 751-775, 2017.HQSpre - An Effective Preprocessor for QBF and DQBF Wimmer, R.; Reimer, S.; Marin, P. and Becker, B.
In Tools and Algorithms for the Construction and Analysis of Systems
- 23rd International Conference, TACAS 2017, Held as Part of the
European Joint Conferences on Theory and Practice of Software, ETAPS
2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I , pages 373-390, Lecture Notes in Computer Science 10205, 2017.Motion planning under partial observability using game-based abstraction Winterer, L.; Junges, S.; Wimmer, R.; Jansen, N.; Topcu, U.; Katoen, J.-P. and Becker, B.
In 56th IEEE Annual Conference on Decision and Control, CDC 2017,
Melbourne, Australia, December 12-15, 2017 , pages 2201-2208, IEEE Distribution-Based Bisimulation for Labelled Markov Processes Yang, P.; Jansen, D. N. and Zhang, L.
In FORMATS , pages 170-186, LNCS 10419, 2017.
2016
Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies Ábrahám, E.; Corzilius, F.; Johnsen, E. B.; Kremer, G. and Mauro, J.
In SETTA , pages 229-245, LNCS 9984, 2016.Effective Static and Dynamic Fault Tree Analysis Bäckström, O.; Butkova, Y.; Hermanns, H.; Krcál, J. and Krcál, P.
In Computer Safety, Reliability, and Security - 35th International Conference,
SAFECOMP 2016, Trondheim, Norway, September 21-23, 2016, Proceedings , pages 266-280, Springer Facets of Software Doping Barthe, G.; D'Argenio, P.; Finkbeiner, B. and Hermanns, H.
In ISoLA , pages 601-608, LNCS 9953, 2016.Effective Static and Dynamic Fault Tree Analysis Bäckström, O.; Butkova, Y.; Hermanns, H.; Krcál, J. and Krcál, P.
In SAFECOMP , pages 266-280, LNCS 9922, 2016.Battery-Aware Scheduling in Low Orbit: The GomX-3 Case Bisgaard, M.; Gerhardt, D.; Hermanns, H.; Krcál, J.; Nies, G. and Stenger, M.
In FM , pages 559-576, LNCS 9995, 2016.Validated Simulation-Based Verification of Delayed Differential Dynamics Chen, M.; Fränzle, M.; Li, Y.; Mosaad, P. N. and Zhan, N.
In FM , pages 137-154, LNCS 9995, 2016.A Two-Way Path Between Formal and Informal Design of Embedded Systems Chen, M.; Ravn, A. P.; Wang, S.; Yang, M. and Zhan, N.
In Unifying Theories of Programming - 6th International Symposium, UTP
2016, Reykjavik, Iceland, June 4-5, 2016, Revised Selected Papers , pages 65-92, Springer A Two-Way Path Between Formal and Informal Design of Embedded Systems Chen, M.; Wang, S.; Yang, M. and Zhan, N.
In UTP , pages 65-92, LNCS 10134, 2016.Probabilistic CTL*: The Deductive Way Dimitrova, R.; Ferrer Fioriti, L. M.; Hermanns, H. and Majumdar, R.
In TACAS , pages 280-298, LNCS 9636, 2016.Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks Dombrowski, C.; Junges, S.; Katoen, J.-P. and Gross, J.
In SRDS , pages 307-316, 2016.Efficient approximation of optimal control for continuous-time Markov
games Fearnley, J.; Rabe, M. N.; Schewe, S. and Zhang, L.
In Inf. Comput. , 247: 106-129, 2016.Deciding Probabilistic Automata Weak Bisimulation: Theory and Practice Ferrer Fioriti, L. M.; Hashemi, V.; Hermanns, H. and Turrini, A.
In Formal Aspects of Computing , 28: 109-143, 2016.Computing reachable sets of linear vector fields revisited Gan, T.; Chen, M.; Li, Y.; Xia, B. and Zhan, N.
In ECC , pages 419-426, 2016.Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF Gan, T.; Dai, L.; Xia, B.; Zhan, N.; Kapur, D. and Chen, M.
In IJCAR , pages 195-212, 2016.Exploiting Robust Optimization for Interval Probabilistic Bisimulation Hahn, E. M.; Hashemi, V.; Hermanns, H. and Turrini, A.
In QEST , pages 55-71, LNCS 9826, 2016.A Simple Algorithm for Solving Qualitative Probabilistic Parity Games Hahn, E. M.; Schewe, S.; Turrini, A. and Zhang, L.
In CAV , pages 291-311, LNCS 9780, 2016.Flexible support for time and costs in scenario-aware dataflow Hartmanns, A.; Hermanns, H. and Bungert, M.
In EMSOFT , pages 3:1-3:10, 2016.Schedulers are no Prophets Hartmanns, A.; Hermanns, H. and Krcál, J.
In Semantics, Logics, and Calculi'16 , pages 214-235, LNCS 9560, 2016.Compositional Bisimulation Minimization for Interval Markov Decision
Processes Hashemi, V.; Hermanns, H.; Song, L.; Subramani, K.; Turrini, A. and Wojciechowski, P. J.
In Language and Automata Theory and Applications - 10th International
Conference, LATA 2016, Prague, Czech Republic, March 14-18, 2016,
Proceedings , pages 114-126, Springer Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes He, F.; Gao, X.; Wang, M.; Wang, B.-Y. and Zhang, L.
In ACM Trans. Softw. Eng. Methodol. , 25: 21:1-21:39, 2016.The Value of Attack-Defence Diagrams Hermanns, H.; Krämer, J.; Krcál, J. and Stoelinga, M.
In POST , pages 163-185, LNCS 9635, 2016.Distributed Synthesis in Continuous Time Hermanns, H.; Krcál, J. and Vester, S.
In FoSSaCS , pages 353-369, LNCS 9634, 2016.Uncovering Dynamic Fault Trees Junges, S.; Guck, D.; Katoen, J.-P. and Stoelinga, M.
In DSN , pages 299-310, 2016.Safety-Constrained Reinforcement Learning for MDPs Junges, S.; Jansen, N.; Dehnert, C.; Topcu, U. and Katoen, J.-P.
In Tools and Algorithms for the Construction and Analysis of Systems
- 22nd International Conference, TACAS 2016, Held as Part of the
European Joint Conferences on Theory and Practice of Software, ETAPS
2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings , pages 130-146, Springer The Probabilistic Model Checking Landscape Katoen, J.-P.
In LICS , pages 31-45, 2016.Towards Concolic Testing for Hybrid Systems Kong, P.; Li, Y.; Chen, X.; Sun, J.; Sun, M. and Wang, J.
In FM , pages 460-478, LNCS 9995, 2016.An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties Li, Y.; Liu, W.; Turrini, A.; Hahn, E. M. and Zhang, L.
In SETTA , pages 280-296, LNCS 9984, 2016.Verify LTL with Fairness Assumptions Efficiently Li, Y.; Song, L.; Feng, Y. and Zhang, L.
In TIME , 2016.Active Learning from Blackbox to Timed Connectors Li, Y.; Sun, M. and Wang, Y.
In TASE , pages 132-135, 2016.Parameter Synthesis for Markov Models: Faster Than Ever Quatmann, T.; Dehnert, C.; Jansen, N.; Junges, S. and Katoen, J.-P.
In ATVA , pages 50-67, Lecture Notes in Computer Science 9938, 2016.Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates Volk, M.; Junges, S. and Katoen, J.-P.
In SAFECOMP , pages 253-265, LNCS 9922, 2016.Skolem Functions for DQBF Wimmer, K.; Wimmer, R.; Scholl, C. and Becker, B.
In ATVA , pages 395-411, LNCS 9938, 2016.GPU-Accelerated Value Iteration for the Computation of Reachability
Probabilities in MDPs Wu, Z.; Hahn, E. M.; Günay, A.; Zhang, L. and Liu, Y.
In ECAI , pages 1726-1727, Frontiers in Artificial Intelligence and Applications 285, 2016.Performance Evaluation of Concurrent Data Structures Wu, H.; Yang, X. and Katoen, J.-P.
In SETTA , pages 38-49, LNCS 9984, 2016.Multiphase until formulas over Markov reward models: An algebraic
approach Xu, M.; Zhang, L.; Jansen, D. N.; Zhu, H. and Yang, Z.
In Theor. Comput. Sci. , 611: 116-135, 2016.Approximate Bisimulation and Discretization of Hybrid CSP Yan, G.; Jiao, L.; Li, Y.; Wang, S. and Zhan, N.
In FM 2016: Formal Methods - 21st International Symposium, Limassol,
Cyprus, November 9-11, 2016, Proceedings , pages 702-720, Lecture Notes in Computer Science 9995, 2016.Reasoning about Connectors in Coq Zhang, X.; Hong, W.; Li, Y. and Sun, M.
In FACS , pages 172-190, LNCS 10231, 2016.A space-efficient simulation algorithm on probabilistic automata Zhang, L. and Jansen, D. N.
In Inf. Comput. , 249: 138-159, 2016.
2015
Rare Event Simulation with Fully Automated Importance Splitting Budde, C. E.; D'Argenio, P. R. and Hermanns, H.
In Computer Performance Engineering - 12th European Workshop, EPEW
2015, Madrid, Spain, August 31 - September 1, 2015, Proceedings , pages 275-290, Springer Optimal Continuous Time Markov Decisions Butkova, Y.; Hatefi, H.; Hermanns, H. and Krcál, J.
In Automated Technology for Verification and Analysis - 13th International
Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings , pages 166-182, Springer Transient Reward Approximation for Continuous-Time Markov Chains Hahn, E. M.; Hermanns, H.; Wimmer, R. and Becker, B.
In IEEE Trans. Reliab. , 64: 1254-1275, 2015.Explicit Model Checking of Very Large MDP Using Partitioning and
Secondary Storage Hartmanns, A. and Hermanns, H.
In Automated Technology for Verification and Analysis - 13th International
Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings , pages 131-147, Springer In the quantitative automata zoo Hartmanns, A. and Hermanns, H.
In Sci. Comput. Program. , 112: 3-23, 2015.Recharging Probably Keeps Batteries Alive Hermanns, H.; Krcál, J. and Nies, G.
In Cyber Physical Systems. Design, Modeling, and Evaluation - 5th International
Workshop, CyPhy 2015, Amsterdam, The Netherlands, October 8, 2015,
Proceedings , pages 83-98, Springer A Framework for Off-Line Conformance Testing of Timed Connectors Li, S.; Chen, X.; Wang, Y. and Sun, M.
In TASE , pages 15-22, 2015.A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking van Dijk, T.; Hahn, E. M.; Jansen, D. N.; Li, Y.; Neele, T.; Stoelinga, M.; Turrini, A. and Zhang, L.
In Dependable Software Engineering, Theories, Tools, and Applications. First International Symposium (SETTA 2015) , pages 35-54, Springer , Lecture Notes in Computer Science 9409, 2015.Polynomial Time Decision Algorithms for Probabilistic Automata Turrini, A. and Hermanns, H.
In Information and Computation , 244: 134-171, 2015.
