A5074733161- Formal Methods in Verification
- semigroups and automata theory
- Software Testing and Debugging Techniques
- Machine Learning and Algorithms
- Logic, Reasoning, and Knowledge
- Logic, programming, and type systems
- Software Reliability and Analysis Research
- Petri Nets in System Modeling
- Software Engineering Research
- Advanced Software Engineering Methodologies
- Quantum Computing Algorithms and Architecture
- Advanced Authentication Protocols Security
- Reinforcement Learning in Robotics
- Bayesian Modeling and Causal Inference
- Distributed systems and fault tolerance
- Model-Driven Software Engineering Techniques
- Web Application Security Vulnerabilities
- Numerical Methods and Algorithms
- Cryptography and Data Security
- Cryptographic Implementations and Security
- Artificial Intelligence in Games
- Access Control and Trust
- AI-based Problem Solving and Planning
- Optimization and Search Problems
- DNA and Biological Computing
Institute of Software
2015-2024
Chinese Academy of Sciences
2015-2024
State Key Laboratory of Computer Science
2017-2019
Saarland University
2013
University of Verona
2005-2010
The bottleneck in the quantitative analysis of Markov chains and decision processes against specifications given LTL or as some form nondeterministic Buchi automata is inclusion a determinisation step automaton under consideration. In this paper, we show that full can be avoided: subset breakpoint constructions suffice. We have implemented our approach - both explicit symbolic versions prototype tool. Our experiments compete with mature tools like PRISM.
In 2014, Heizmann et al. proposed a novel framework for program termination analysis. The analysis starts with proof of sample path. path is generalized to Büchi automaton (BA) whose language (by construction) represents set terminating paths. All these paths can be safely removed from the program. removal done using automata difference, implemented via BA complementation and intersection. constructs in this way BAs that jointly "cover" behavior program, thus proving its termination. An...
We consider bisimulation and weak relations in the context of labeled Markov chains Hansson Jonsson, concurrent Philippou, Lee, Sokolsky, probabilistic automata Segala. identify a taxonomy that captures existing definitions for each one three models, we compare within model across models. The comparison models is given according to notion embedding, where order by generality view objects less general as more
Accurate Modelling of a real-world system with probabilistic behaviour is difficult task. Sensor noise and statistical estimations, among other imprecisions, make the exact probability values impossible to obtain. In this article, we consider Interval Markov decision processes ( IMDP s), which generalise classical MDP s by having interval-valued transition probabilities. They provide powerful modelling tool for systems an additional variation or uncertainty that prevents knowledge We...
We study simulation relations for probabilistic automata that require transitions to be matched up negligible sets provided computation lengths are polynomially bounded. These meant provide rigorous grounds parts of correctness proofs cryptographic protocols usually carried out by semi-formal arguments. illustrate our ideas recasting a proof Bellare and Rogaway based on the notion matching conversation.
Deciding in an efficient way weak probabilistic bisimulation the context of automata is open problem for about a decade. In this work we close by proposing procedure that checks polynomial time existence combined transition satisfying step condition bisimulation. This enables us to arrive at algorithm deciding We also present several extensions interesting related problems setting ground development more effective and compositional analysis algorithms systems.
Quantum Markov chains are an extension of classical which labelled with super-operators rather than probabilities. They allow to faithfully represent quantum programs and protocols. In this paper, we investigate model checking omega-regular properties, a very general class properties (including, e.g., LTL properties) interest, against model. For chains, such usually checked by building the product language automaton. Subsequent analysis is then performed on product. When doing so, one...
In this work we study the model checking problem for probabilistic multiagent systems with respect to epistemic logic PETL, which can specify both temporal and properties. We show that under realistic assumption of uniform schedulers, i.e., choice every agent depends only on its observation history, PETL is undecidable. By restricting class schedulers be memoryless becomes decidable. More importantly, design a novel algorithm reduces into mixed integer non-linear programming problem, then...
The bottleneck in the quantitative analysis of Markov chains and decision processes against specifications given LTL or as some form nondeterministic Büchi automata is inclusion a determinisation step automaton under consideration. In this paper, we show that full can be avoided: subset breakpoint constructions suffice. We have implemented our approach---both explicit symbolic versions---in prototype tool. Our experiments compete with mature tools like PRISM.