A general definition of a quantum predicate and quantum labelled transition systems for finite quantum computation systems is presented. The notion of a quantum predicate as a positive operator-valued measure is developed. The main results of this paper are a theorem about the existence of generalised predicates for quantum programs defined as completely positive maps and a theorem about the existence of a GSOS format for quantum labelled transition systems. The first theorem is a slight generalisation...

We investigate the possibility of extending Chrobak normal form to the probabilistic case. While in the nondeterministic case a unary automaton can be simulated by an automaton in Chrobak normal form without increasing the number of the states in the cycles, we show that in the probabilistic case the simulation is not possible by keeping the same number of ergodic states. This negative result is proved by considering the natural extension to the...

We investigate the possibility of extending Chrobak normal form to the probabilistic case. While in the nondeterministic case a unary automaton can be simulated by an automaton in Chrobak normal form without increasing the number of the states in the cycles, we show that in the probabilistic case the simulation is not possible by keeping the same number of ergodic states. This negative result is proved by considering the natural extension to the probabilistic case of Chrobak normal form, obtained...

We investigate the possibility of extending Chrobak normal form to the probabilistic case. While in the nondeterministic case a unary automaton can be simulated by an automaton in Chrobak normal form without increasing the number of the states in the cycles, we show that in the probabilistic case the simulation is not possible by keeping the same number of ergodic states. This negative result is proved by considering the natural extension to the...

We investigate the succinctness of several kinds of unary automata by studying their state complexity in accepting the family $\left\{L_m\right\}$ of cyclic languages, where $L_m=\left\{a^{km}\right|k\in \mathbb{N}\}$. In particular, we show that, for any $m$, the number of states necessary and sufficient for accepting the unary language $L_m$ with isolated cut point on one-way probabilistic finite automata is $p_1^{{\alpha }_1}+p_2^{{\alpha }_2}+\cdots +p_s^{{\alpha }_s}$, with $p_1^{{\alpha }_1}{p}_2^{{\alpha }_2}\cdots p_s^{{\alpha }_s}$ being the factorization of $m$. To prove this result, we give a general state lower bound for accepting unary languages with isolated cut point on...

We investigate the succinctness of several kinds of unary automata by studying their state complexity in accepting the family {Lm} of cyclic languages, where Lm = akm | k ∈ N. In particular, we show that, for any m, the number of states necessary and sufficient for accepting the unary language Lm with isolated cut point on one-way probabilistic finite automata is $p_1^{{\alpha }_1}+p_2^{{\alpha }_2}+\cdots +p_s^{{\alpha }_s}$, with $p_1^{{\alpha }_1}{p}_2^{{\alpha }_2}\cdots p_s^{{\alpha }_s}$ being the factorization of m. To prove this result, we give a general state lower bound for accepting unary languages...