Search

For many applications, we are unable to take full advantage of the potential massive parallelisation offered by supercomputers or cloud computing because it is too hard to work out how to divide up the computation task between processors in such a way to minimise the need for communication. However, a recently developed branch-independent tableaux for the common LTL temporal logic should intuitively be easy to parallelise as each branch can be developed independently. Here we describe a simple technique for partitioning such a tableau such that each partition can be processed independently without need for interprocess communication. We investigate the extent to which this technique improves the performance of the LTL tableau on standard benchmarks and random formulas., Comment: In Proceedings GandALF 2017, arXiv:1709.01761

This paper proposes a new logic RoCTL* to model robustness in concurrent systems. RoCTL* extends CTL* with the addition of Obligatory and Robustly operators, which quantify over failure-free paths and paths with one more failure respectively. We present a number of examples of problems to which RoCTL* can be applied. The core result of this paper is to show that RoCTL* is expressively equivalent to CTL* but is non-elementarily more succinct. We present a translation from RoCTL* into CTL* that preserves truth but may result in non-elementary growth in the length of the translated formula as each nested Robustly operator may result in an extra exponential blowup. However, we show that this translation is optimal in the sense that any equivalence preserving translation will require an extra exponential growth per nested Robustly. We also compare RoCTL* to Quantified CTL* (QCTL*) and hybrid logics.

We use Hotelling's spatial model of competition to investigate the position-taking behaviour of political candidates under a class of electoral systems known as scoring rules. In a scoring rule election, voters rank all the candidates running for office, following which the candidates are assigned points according to a vector of nonincreasing scores. Convergent Nash equilibria in which all candidates adopt the same policy were characterised by Cox (1987). Here, we investigate nonconvergent equilibria, where candidates adopt divergent policies. We identify a number of classes of scoring rules exhibiting a range of different equilibrium properties. For some of these, nonconvergent equilibria do not exist. For others, nonconvergent equilibria in which candidates cluster at positions spread across the issue space are observed. In particular, we prove that the class of convex rules does not have Nash equilibria (convergent or nonconvergent) with the exception of some derivatives of Borda rule. Finally, we examine the special cases of four-, five- and six- candidate elections. In the former two cases, we provide a complete characterisation of nonconvergent equilibria.

With the Dodgson rule, cloning the electorate can change the winner, which Young (1977) considers an "absurdity". Removing this absurdity results in a new rule (Fishburn, 1977) for which we can compute the winner in polynomial time (Rothe et al., 2003), unlike the traditional Dodgson rule. We call this rule DC and introduce two new related rules (DR and D&). Dodgson did not explicitly propose the "Dodgson rule" (Tideman, 1987); we argue that DC and DR are better realizations of the principle behind the Dodgson rule than the traditional Dodgson rule. These rules, especially D&, are also effective approximations to the traditional Dodgson's rule. We show that, unlike the rules we have considered previously, the DC, DR and D& scores differ from the Dodgson score by no more than a fixed amount given a fixed number of alternatives, and thus these new rules converge to Dodgson under any reasonable assumption on voter behaviour, including the Impartial Anonymous Culture assumption., Comment: Expanded draft of paper presented at COMSOC 2008