Vol 42, No 4 (2016)

In the paper, a “truly concurrent” and nondeterministic semantics is defined in terms of branching processes of discrete-time Petri nets (DTPNs). These nets may involve infinite numbers of transitions and places, infinite number of tokens in places, and (maximal) steps of concurrent transitions, which allows us to consider this class of DTPNs to be the most powerful class of Petri nets. It is proved that the unfolding (maximal branching process) of the DTPN is the greatest element of a complete lattice constructed on branching processes of DTPNs with step semantics. Moreover, it is shown that this result is true also in the case of maximal transition steps if additional restrictions are imposed on the structure and behavior of the DTPN.

The paper presents a conflict resolution algorithm for multi-agent systems with agents connected by relations of different types and worth. The result of conflict resolution is a conflict-free set of agents. We apply this algorithm for the ambiguity resolution problem in ontology population based on multiagent natural language text analysis.

Currently, static verifiers based on counterexample-guided abstraction refinement (CEGAR) can prove correctness of a program against a specified requirement, find its violation in a program, and stop analysis or exhaust the given resources without producing any useful result. Theoretically, we could use this approach for checking several requirements at once; however, finding of the first violation of some requirement or exhausting resources for some requirement will prevent from checking the program against other requirements. Moreover, if the program contains more than one violation of the requirement, CEGAR will find only the very first violation and may miss potential errors in the program. At the same time, static verifiers perform similar actions during checking of the same program against different requirements, which results in waste of a lot of resources. This paper presents a new CEGAR-based method for software static verification, which is aimed at checking programs against several requirements at once and getting the same result as basic CEGAR checking requirements one by one. To achieve this goal, the suggested method distributes resources over requirements and continues analysis after finding a violation of a requirement. We used Linux kernel modules to conduct experiments, in which implementation of the suggested method reduced total verification time by five times. The total number of divergent results in comparison with the base CEGAR was about 2%. Having continued the analysis after finding the first violation, this method guarantees that all violations of given requirements are found in 40% of cases, with the number of violations found being 1.5 times greater than in that in the base CEGAR approach.