A logical duality for underspecified probabilistic systems

This paper establishes a Stone-type duality between specifications and infLMPs. An infLMP is a probabilistic process whose transitions satisfy super-additivity instead of additivity. Interestingly, its simple structure can encode a mix of probabilistic and non-deterministic behavior, which, as we show, is strongly related to another well-known such model: probabilistic automata. Our duality puts in relation the category of infLMPs and a category of abstract representations of them based on properties only. We exhibit a Galois connection between these categories and show that we have an adjunct pair of functors when restricted to LMPs only. Our duality also shows that an infLMP can be considered as a demonic representative of a system’s information. Moreover, it carries forward a view where states are less important, and events, or properties, become the main characters, as it should be in probability theory. Along the way, we show that bisimulation and simulation are naturally interpreted in this setting, and we exhibit the interesting relationship between infLMPs and the usual probabilistic modal logics. This paper is an extended version of a Concur ’09 paper [13]; in particular, the comparison of infLMPs with probabilistic automata and the Galois connection are new.     

Bisimulation and cocongruence for probabilistic systems

We introduce a new notion of bisimulation, called event bisimulation on labelled Markov processes (LMPs) and compare it with the, now standard, notion of probabilistic bisimulation, originally due to Larsen and Skou. Event bisimulation uses a sub σ-algebra as the basic carrier of information rather than an equivalence relation. The resulting notion is thus based on measurable subsets rather than on points: hence the name. Event bisimulation applies smoothly for general measure spaces; bisimulation, on the other hand, is known only to work satisfactorily for analytic spaces. We prove the logical characterization theorem for event bisimulation without having to invoke any of the subtle aspects of analytic spaces that feature prominently in the corresponding proof for ordinary bisimulation. These complexities only arise when we show that on analytic spaces the two concepts coincide. We show that the concept of event bisimulation arises naturally from taking the co-congruence point of view for probabilistic systems. We show that the theory can be given a pleasing categorical treatment in line with general coalgebraic principles. As an easy application of these ideas we develop a notion of “almost sure” bisimulation; the theory comes almost “for free” once we modify Giry’s monad appropriately.     

Bisimulation for Labelled Markov Processes

In this paper we introduce a new class of labelled transition systems—labelled Markov processes— and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete. We assume that the state space is a certain type of common metric space called an analytic space. We show that our definition of probabilistic bisimulation generalizes the Larsen–Skou definition given for discrete systems. The formalism and mathematics is substantially different from the usual treatment of probabilistic process algebra. The main technical contribution of the paper is a logical characterization of probabilistic bisimulation. This study revealed some unexpected results, even for discrete probabilistic systems.

• Bisimulation can be characterized by a very weak modal logic. The most striking feature is that one has no negation or any kind of negative proposition.

• We do not need any finite branching assumption, yet there is no need of infinitary conjunction.

We also show how to construct the maximal autobisimulation on a system. In the finite state case, this is just a state minimization construction. The proofs that we give are of an entirely different character than the typical proofs of these results. They use quite subtle facts about analytic spaces and appear, at first sight, to be entirely nonconstructive. Yet one can give an algorithm for deciding bisimilarity of finite state systems which constructs a formula that witnesses the failure of bisimulation.     

Using bisimulation proof techniques for the analysis of distributed abstract machines

We illustrate the use of recently developed proof techniques for weak bisimulation by analysing a generic framework for the definition of distributed abstract machines based on a message-passing implementation. We first define this framework, and then focus on the algorithm which is used to route messages asynchronously to their destination.A first version of this algorithm can be analysed using the standard bisimulation up to expansion proof technique. We show that in a second, optimised version, rather complex behaviours appear, for which more sophisticated techniques, relying on termination arguments, are necessary to establish behavioural equivalence.     

Interval‐valued probabilistic linguistic term sets in multi‐criteria group decision making

The theory of probabilistic linguistic term sets (PLTSs) is very useful in objectively dealing with the multi‐criteria group decision making (MCGDM) problems in which there is hesitancy in providing linguistic assessments; and PLTSs allow experts to express their preferences on one linguistic term over another. In order to reflect the uncertainty and inconsistency of decision‐makers and handle incomplete linguistic information, we propose a new PLTS called interval‐valued probabilistic linguistic term set (IVPLTS). In addition, the existing approaches associated with PLTSs are limited or highly complex in real applications. Therefore, new operations, comparison laws, and aggregation operators are developed for IVPLTS. Furthermore, we establish an efficient framework for MCGDM problems based on the proposed comparison method and the fuzzy preference relation. Then we apply it to a real‐life case under linguistic environment. The extended TOPSIS methods combined with PLTSs by using different operational laws are also included for comparison. The final results demonstrate the efficiency and practicality of the new framework.     

基于可能度矩阵的概率语言多属性决策方法

为解决两个概率语言术语集之间的优劣比较这一基本问题,在已有可能度计算方法的基础上,提出一种改进的可能度公式.该可能度公式能够克服已有可能度公式的缺点,具有计算过程简单、区分能力强、易于拓展应用等特点.进一步研究发现:基于该可能度公式对多个评估对象进行两两比较得到的可能度矩阵,具有加性一致性的模糊互补偏好关系;将多个可能度矩阵加权平均得到的综合可能度矩阵,也具有加性一致性的模糊互补偏好关系.据此,构建一种概率语言多属性决策方法,并将其应用于军队院校教育教学质量评价.数值实验表明,所提出的概率语言多属性决策方法结构简单、计算过程清晰且具有较强的自检能力,能够通过确保计算过程的正确性来保证决策结果的有效性.     

Metrics for Action-labelled Quantitative Transition Systems

This paper defines action-labelled quantitative transition systems as a general framework for combining qualitative and quantitative analysis. We define state-metrics as a natural extension of bisimulation from non-quantitative systems to quantitative ones. We then prove that any single state-metric corresponds to a bisimulation and that the greatest state-metric corresponds to bisimilarity. Furthermore, we provide two extended examples which show that our results apply to both probabilistic and weighted automata as special cases of action-labelled quantitative transition systems.     

A new method for probabilistic linguistic multi-attribute group decision making: Application to the selection of financial technologies

“No technology, no finance” has been the consensus in banking industry. Under the background of financial technology (Fintech), how to select an appropriate technology company to cooperate for the banks has become a key. The technology company selection can be regarded as a kind of multi-attribute group decision making (MAGDM) problems. The probabilistic linguistic term set (PLTS) is a useful tool to express decision makers’ (DMs’) evaluations in the technology company selection. This paper develops a new method for MAGDM with PLTSs. Firstly, the possibility degree and range value of PLTSs are defined. Then a possibility degree algorithm is designed for ranking PLTSs. An Euclidean distance measure between PLTSs is presented and extended to probabilistic linguistic matrices. Based on Archimedean t-norm and s-norm, some new operational laws for PLTSs are defined and some desirable properties are discussed. Then, a generalized probabilistic linguistic Hamacher weighted averaging (GPLHWA) operator and a generalized probabilistic linguistic Hamacher ordered weighted averaging (GPLHOWA) operator are developed. Some useful properties for these operators are investigated in detail. Combined with the subjective weights of DMs, the DMs’ weights are determined by the adjusted coefficients. Using the GPLHWA operator, the collective decision matrix is obtained by aggregating all the individual decision matrices. By maximizing the total weighted square possibility degree, a multi-objective program is constructed to derive the attribute weights. The ranking order of alternatives is generated by integrating ELECTRE and TOPSIS. Thereby, a new method is put forward for MAGDM with PLTSs. A Fintech example is analyzed to show the effectiveness of the proposed method. The sensitivity analysis and comparative analyses are conducted to illustrate its advantages.     

Operators and comparisons of probabilistic linguistic term sets

The probabilistic linguistic term sets (PLTSs) allow experts to express their preferences regarding one linguistic term over another. Nowadays, multicriteria decision-making methods for PLTSs are very popular, and Bai et al’s multicriteria decision-making method based on the possibility degree formula for PLTSs cannot be ranked in some situations. In this paper, we first propose a new possibility degree method for PLTSs and state their properties, and we use this new possibility degree method to solve the drawbacks of Bai et al’s possibility degree method. Second, we propose a probabilistic linguistic weight average (PLWA) and probabilistic linguistic order weight average (PLOWA) operator and state their properties. Then, based on the new possibility degree method and the PLWA (PLOWA) operator, we propose a multicriteria decision-making method based the PLWA (PLOWA) operator. Finally, we utilize an example to illustrate the interrelationships between our method and Bai et al’s method. The result shows that our multicriteria decision-making method is more rational.     

Decision procedures and graph reductions for bisimulation equivalences part 1

In Process Algebra, processes are often specified in a framework of bisimulation semantics. The notion of bisimulation therefore plays an important role.

In this paper some existing and new decision methods are presented for strong bisimulation, τ-bisimulation and η-bisimulation. Each of these bisimulation equivalences corresponds to a certain abstraction mechanism.

In strong bisimulation, all events in a system are treated equally whereas τ-bisimulation takes into account the silent step τ; η-bisimulation was introduced recently for an alternative silent step η that is less abstract than τ. It is shown that the problem of η-bisimulation decision can be reduced to an abstract graph partitioning problem called the Product Relational Coarsest Partition problem. Special attention is paid to computational complexity of the decision methods.

As it turns out. finite process graphs can be reduced to unique minimal normalforms under all three bisimulation semantics mentioned.

The last section demonstrates how the decision methods can be used with a particular algebraic model to enable effective verification of specifications.     

Deciding probabilistic automata weak bisimulation: theory and practice

Weak probabilistic bisimulation on probabilistic automata can be decided by an algorithm that needs to check a polynomial number of linear programming problems encoding weak transitions. It is hence of polynomial complexity. This paper discusses the specific complexity class of the weak probabilistic bisimulation problem, and it considers several practical algorithms and linear programming problem transformations that enable an efficient solution. We then discuss two different implementations of a probabilistic automata weak probabilistic bisimulation minimizer, one of them employing SAT modulo linear arithmetic as the solver technology. Empirical results demonstrate the effectiveness of the minimization approach on standard benchmarks, also highlighting the benefits of compositional minimization.     

Probabilistic approximation of runtime quantitative verification in self-adaptive systems

Cyber-physical systems (CPS) are expected to continuously monitor the physical components to autonomously calculate appropriate runtime reactions to deal with the uncertain environmental conditions. Self-adaptation, as a promising concept to fulfill a set of provable rules, majorly needs runtime quantitative verification (RQV). Taking a few probabilistic variables into account to represent the uncertainties, the system configuration will be extremely large. Thus, efficient approaches are needed to reduce the model state-space, preferably with certain bounds on the approximation error. In this paper, we propose an approximation framework to efficiently approximate the entire model of a self-adaptive system. We split up the large model into strongly-connected components (SCCs), apply the approximation algorithm separately on each SCC, and integrate the result of each part using a centralized algorithm. Due to a number of changes in probabilistic variables, it is not possible to use static models. Addressing this issue, we have deployed parametric Markov decision process. In order to apply approximation on the model, the notion of ε-approximate probabilistic bisimulation is utilized that introduces the approximation level ε. We show that our approximation framework offers a certain error bound on each level of approximation. Then, we denote that the approximation framework is appropriate to be applied in decision-making process of self-adaptive systems where the models are relatively large. The results reveal that we can achieve up to 50% size reduction in the approximate model while maintaining the accuracy about 95%. In addition, we discuss about the trade-off between efficiency and accuracy of our approximation framework.     

Probabilistic Logical Characterization

Probabilistic automata exhibit both probabilistic and non-deterministic choice. They are therefore a powerful semantic foundation for modeling concurrent systems with random phenomena arising in many applications ranging from artificial intelligence, security, systems biology to performance modeling. Several variations of bisimulation and simulation relations have proved to be useful as means to abstract and compare different automata. This paper develops a taxonomy of logical characterizations of these relations on image-finite and image-infinite probabilistic automata.     

Structured coalgebras and minimal HD-automata for the -calculus

The coalgebraic framework developed for the classical process algebras, and in particular its advantages concerning minimal realizations, does not fully apply to the π-calculus, due to the constraints on the freshly generated names that appear in the bisimulation.In this paper we propose to model the transition system of the π-calculus as a coalgebra on a category of name permutation algebras and to define its abstract semantics as the final coalgebra of such a category. We show that permutations are sufficient to represent in an explicit way fresh name generation, thus allowing for the definition of minimal realizations.We also link the coalgebraic semantics with a slightly improved version of history dependent (HD) automata, a model developed for verification purposes, where states have local names and transitions are decorated with names and name relations. HD-automata associated with agents with a bounded number of threads in their derivatives are finite and can be actually minimized. We show that the bisimulation relation in the coalgebraic context corresponds to the minimal HD-automaton.     

Z‐uncertain probabilistic linguistic variables and its application in emergency decision making for treatment of COVID‐19 patients

Probabilistic linguistic term sets (PLTSs) have many applications in the field of group decision making (GDM) because it includes both linguistic evaluation and probabilistic distribution when expressing preference information. However, the difference of information credibility in PLTSs is ignored, resulting in an inaccurate representation of decision information and unreasonable probability calculation. In this paper, we first consider the credibility of the information and propose the concept of Z‐uncertain probabilistic linguistic variables (Z‐UPLVs). Subsequently, the operational rules, normalization, distance and similarity measures, and comparison method of Z‐UPLVs are introduced. Then, a probability calculation method based on credibility, an extended TOPSIS method, and some operators are proposed, which can be applied to emergency decision making in the Z‐uncertain probabilistic linguistic (Z‐UPL) environment. Finally, an emergency decision‐making case of COVID‐19 patients and comparative analysis illustrate the necessity and effectiveness of this method.     

Deciding orthogonal bisimulation

Bergstra, Ponse and van der Zwaag introduced in 2003 the notion of orthogonal bisimulation equivalence on labeled transition systems. This equivalence is a refinement of branching bisimulation, in which consecutive tau’s (silent steps) can be compressed into one (but not zero) tau’s. The main advantage of orthogonal bisimulation is that it combines well with priorities. Here we solve the problem of deciding orthogonal bisimulation equivalence in finite (regular) labeled transition systems. Unlike as in branching bisimulation, in orthogonal bisimulation, cycles of silent steps cannot be eliminated. Hence, the algorithm of Groote and Vaandrager (1990) cannot be adapted easily. However, we show that it is still possible to decide orthogonal bisimulation with the same complexity as that of Groote and Vaandrager’s algorithm. Thus if n is the number of states, and m the number of transitions then it takes O(n(m + n)) time to decide orthogonal bisimilarity on finite labeled transition systems, using O(m + n) space. J. Parrow     

Exploring probabilistic bisimulations, part I

We take a fresh look at strong probabilistic bisimulations for processes which exhibit both non-deterministic and probabilistic behaviour. We suggest that it is natural to interpret such processes as distributions over states in a probabilistic labelled transition system, a pLTS; this enables us to adapt the standard notion of contextual equivalence to this setting. We then prove that a novel form of bisimulation equivalence between distributions are both sound and complete with respect to this contextual equivalence. We also show that a very simple extension to HML, Hennessy–Milner Logic, provides finite explanations for inequivalences between distributions. Finally we show that our bisimulations between distributions in a pLTS are simply an alternative characterisation of a standard notion of probabilistic bisimulation equivalence, defined between states in a pLTS.     

Weak bisimulation for Probabilistic Timed Automata

We are interested in describing timed systems that exhibit probabilistic behaviour. To this purpose, we consider a model of Probabilistic Timed Automata and introduce a concept of weak bisimulation for these automata, together with an algorithm to decide it. The weak bisimulation relation is shown to be preserved when either time, or probability is abstracted away. As an application, we use weak bisimulation for Probabilistic Timed Automata to model and analyze a timing attack on the dining cryptographers protocol.     

Branching Bisimulation Congruence for Probabilistic Systems

The notion of branching bisimulation for the alternating model of probabilistic systems is not a congruence with respect to parallel composition. In this paper we first define another branching bisimulation in the more general model allowing consecutive probabilistic transitions, and we prove that it is compatible with parallel composition. We then show that our bisimulation is actually the coarsest congruence relation included in the existing branching bisimulation when restricted to the alternating model.     

From Bisimulation to Simulation: Coarsest Partition Problems

The notions of bisimulation and simulation are used for graph reduction and are widely employed in many areas: modal logic, concurrency theory, set theory, formal verification, and so forth. In particular, in the context of formal verification they are used to tackle the so-called state-explosion problem. The faster algorithms to compute the maximum bisimulation on a given labeled graph are based on the crucial equivalence between maximum bisimulation and relational coarsest partition problem. As far as simulation is concerned, many algorithms have been proposed that turn out to be relatively inexpensive in terms of either time or space. In this paper we first revisit the state of the art about bisimulation and simulation, pointing out the analogies and differences between the two problems. Then, we propose a generalization of the relational coarsest partition problem, which is equivalent to the simulation problem. Finally, we present an algorithm that exploits such a characterization and improves on previously proposed algorithms for simulation. This revised version was published online in August 2006 with corrections to the Cover Date.