Petri网可达性的综合判定法

Petri网标识的可达性判定问题是进行Petri网分析的基础,而传统的判定方法并不能确保所得结果的可靠性.在揭示Petri网可达性问题的实质之后,讨论了在标识图的同一连通域内标识可达性的判定问题,进而在分析相关原理的基础上提出了一种有效判定Petri网标识可达性的综合判定法.此判定方法综合多种传统判定方法的优点,结合Gr鯾ner基理论,确保了对Petri网标识可达性进行判定所得结果的可靠性.

Algorithmique et complexité des systèmes à compteurs

Réalisé en cotutelle avec l'École normale supérieure de Cachan – Université Paris-Saclay

Algorithmique et complexité des systèmes à compteurs

Réalisé en cotutelle avec l'École normale supérieure de Cachan – Université Paris-Saclay

Checking Liveness Properties of Presburger Counter Systems Using Reachability Analysis

Counter systems are a well-known and powerful modeling notation for specifying infinite-state systems. In this paper we target the problem of checking liveness properties in counter systems. We propose two semi decision techniques towards this, both of which return a formula that encodes the set of reachable states of the system that satisfy a given liveness property. A novel aspect of our techniques is that they use reachability analysis techniques, which are well studied in the literature, as black boxes, and are hence able to compute precise answers on a much wider class of systems than previous approaches for the same problem. Secondly, they compute their results by iterative expansion or contraction, and hence permit an approximate solution to be obtained at any point. We state the formal properties of our techniques, and also provide experimental results using standard benchmarks to show the usefulness of our approaches. Finally, we sketch an extension of our liveness checking approach to check general CTL properties.

An Efficient and Verifiable Solution to the Millionaire Problem

A new solution to the millionaire problem is designed on the base of two new techniques: zero test and batch equation. Zero test is a technique used to test whether one or more ciphertext contains a zero without revealing other information. Batch equation is a technique used to test equality of multiple integers. Combination of these two techniques produces the only known solution to the millionaire problem that is correct, private, publicly verifiable and efficient at the same time.