bluuebunny/crossref_metadata_2025 huggingface dataset:
Essential Convexity and Complexity of Semi-Algebraic Constraints
Authors: Bodirsky Manuel , Jonsson Peter , von Oertzen Timo
Published: November 2013

Let \Gamma be a structure with a finite relational signature and a
first-order definition in (R;*,+) with parameters from R, that is, a relational
structure over the real numbers where all relations are semi-algebraic sets. In
this article, we study the computational complexity of constraint satisfaction
problem (CSP) for \Gamma: the problem to decide whether a given primitive
positive sentence is true in \Gamma. We focus on those structures \Gamma that
contain the relations \leq, {(x,y,z) | x+y=z} and {1}. Hence, all CSPs studied
in this article are at least as expressive as the feasibility problem for
linear programs. The central concept in our investigation is essential
convexity: a relation S is essentially convex if for all a,b\inS, there are
only finitely many points on the line segment between a and b that are not in
S. If \Gamma contains a relation S that is not essentially convex and this is
witnessed by rational points a,b, then we show that the CSP for \Gamma is
NP-hard. Furthermore, we characterize essentially convex relations in logical
terms. This different view may open up new ways for identifying tractable
classes of semi-algebraic CSPs. For instance, we show that if \Gamma is a
first-order expansion of (R;*,+), then the CSP for \Gamma can be solved in
polynomial time if and only if all relations in \Gamma are essentially convex
(unless P=NP).
Parameterised Multiparty Session Types
Authors: Denielou Pierre-Malo , Yoshida Nobuko , Bejleri Andi , Hu Raymond
Published: November 2013

For many application-level distributed protocols and parallel algorithms, the
set of participants, the number of messages or the interaction structure are
only known at run-time. This paper proposes a dependent type theory for
multiparty sessions which can statically guarantee type-safe, deadlock-free
multiparty interactions among processes whose specifications are parameterised
by indices. We use the primitive recursion operator from G\"odel's System T to
express a wide range of communication patterns while keeping type checking
decidable. To type individual distributed processes, a parameterised global
type is projected onto a generic generator which represents a class of all
possible end-point types. We prove the termination of the type-checking
algorithm in the full system with both multiparty session types and recursive
types. We illustrate our type theory through non-trivial programming and
verification examples taken from parallel algorithms and Web services usecases.
On Berry's conjectures about the stable order in PCF
Authors: Müller Fritz
Published: November 2013

PCF is a sequential simply typed lambda calculus language. There is a unique
order-extensional fully abstract cpo model of PCF, built up from equivalence
classes of terms. In 1979, G\'erard Berry defined the stable order in this
model and proved that the extensional and the stable order together form a
bicpo. He made the following two conjectures: 1) "Extensional and stable order
form not only a bicpo, but a bidomain." We refute this conjecture by showing
that the stable order is not bounded complete, already for finitary PCF of
second-order types. 2) "The stable order of the model has the syntactic order
as its image: If a is less than b in the stable order of the model, for finite
a and b, then there are normal form terms A and B with the semantics a, resp.
b, such that A is less than B in the syntactic order." We give counter-examples
to this conjecture, again in finitary PCF of second-order types, and also
refute an improved conjecture: There seems to be no simple syntactic
characterization of the stable order. But we show that Berry's conjecture is
true for unary PCF. For the preliminaries, we explain the basic fully abstract
semantics of PCF in the general setting of (not-necessarily complete) partial
order models (f-models.) And we restrict the syntax to "game terms", with a
graphical representation.
Bisimilarity on Basic Process Algebra is in 2-ExpTime (an explicit proof)
Authors: Jancar Petr
Published: November 2013

Burkart, Caucal, Steffen (1995) showed a procedure deciding bisimulation
equivalence of processes in Basic Process Algebra (BPA), i.e. of sequential
processes generated by context-free grammars. They improved the previous
decidability result of Christensen, H\"uttel, Stirling (1992), since their
procedure has obviously an elementary time complexity and the authors claim
that a close analysis would reveal a double exponential upper bound. Here a
self-contained direct proof of the membership in 2-ExpTime is given. This is
done via a Prover-Refuter game which shows that there is an alternating Turing
machine deciding the problem in exponential space. The proof uses similar
ingredients (size-measures, decompositions, bases) as the previous proofs, but
one new simplifying factor is an explicit addition of infinite regular strings
to the state space. An auxiliary claim also shows an explicit exponential upper
bound on the equivalence level of nonbisimilar normed BPA processes. The
importance of clarifying the 2-ExpTime upper bound for BPA bisimilarity has
recently increased due to the shift of the known lower bound from PSpace (Srba,
2002) to ExpTime (Kiefer, 2012).
L-Recursion and a new Logic for Logarithmic Space
Authors: Grohe Martin , Grußien Berit , Hernich André , Laubner Bastian
Published: November 2013

We extend first-order logic with counting by a new operator that allows it to
formalise a limited form of recursion which can be evaluated in logarithmic
space. The resulting logic LREC has a data complexity in LOGSPACE, and it
defines LOGSPACE-complete problems like deterministic reachability and Boolean
formula evaluation. We prove that LREC is strictly more expressive than
deterministic transitive closure logic with counting and incomparable in
expressive power with symmetric transitive closure logic STC and transitive
closure logic (with or without counting). LREC is strictly contained in
fixed-point logic with counting FPC. We also study an extension LREC= of LREC
that has nicer closure properties and is more expressive than both LREC and
STC, but is still contained in FPC and has a data complexity in LOGSPACE. Our
main results are that LREC captures LOGSPACE on the class of directed trees and
that LREC= captures LOGSPACE on the class of interval graphs.
Collapsible Pushdown Graphs of Level 2 are Tree-Automatic
Authors: Kartzow Alexander
Published: November 2013

We show that graphs generated by collapsible pushdown systems of level 2 are
tree-automatic. Even if we allow epsilon-contractions and reachability
predicates (with regular constraints) for pairs of configurations, the
structures remain tree-automatic whence their first-order logic theories are
decidable. As a corollary we obtain the tree-automaticity of the second level
of the Caucal-hierarchy.
Unifying B\"uchi Complementation Constructions
Authors: Fogarty Seth J. , Kupferman Orna , Wilke Thomas , Vardi Moshe Y.
Published: November 2013

Complementation of B\"uchi automata, required for checking automata
containment, is of major theoretical and practical interest in formal
verification. We consider two recent approaches to complementation. The first
is the rank-based approach of Kupferman and Vardi, which operates over a DAG
that embodies all runs of the automaton. This approach is based on the
observation that the vertices of this DAG can be ranked in a certain way,
termed an odd ranking, iff all runs are rejecting. The second is the
slice-based approach of K\"ahler and Wilke. This approach tracks levels of
"split trees" - run trees in which only essential information about the history
of each run is maintained. While the slice-based construction is conceptually
simple, the complementing automata it generates are exponentially larger than
those of the recent rank-based construction of Schewe, and it suffers from the
difficulty of symbolically encoding levels of split trees. In this work we
reformulate the slice-based approach in terms of run DAGs and preorders over
states. In doing so, we begin to draw parallels between the rank-based and
slice-based approaches. Through deeper analysis of the slice-based approach, we
strongly restrict the nondeterminism it generates. We are then able to employ
the slice-based approach to provide a new odd ranking, called a retrospective
ranking, that is different from the one provided by Kupferman and Vardi. This
new ranking allows us to construct a deterministic-in-the-limit rank-based
automaton with a highly restricted transition function. Further, by phrasing
the slice-based approach in terms of ranks, our approach affords a simple
symbolic encoding and achieves the tight bound of Schewe's construction
An Algebraic Preservation Theorem for Aleph-Zero Categorical Quantified Constraint Satisfaction
Authors: Chen Hubie , Müller Moritz
Published: November 2013

We prove an algebraic preservation theorem for positive Horn definability in
aleph-zero categorical structures. In particular, we define and study a
construction which we call the periodic power of a structure, and define a
periomorphism of a structure to be a homomorphism from the periodic power of
the structure to the structure itself. Our preservation theorem states that,
over an aleph-zero categorical structure, a relation is positive Horn definable
if and only if it is preserved by all periomorphisms of the structure. We give
applications of this theorem, including a new proof of the known complexity
classification of quantified constraint satisfaction on equality templates.
Polylogarithmic Cuts in Models of V^0
Authors: Müller Sebastian
Published: November 2013

We study initial cuts of models of weak two-sorted Bounded Arithmetics with
respect to the strength of their theories and show that these theories are
stronger than the original one. More explicitly we will see that
polylogarithmic cuts of models of $\mathbf{V}^0$ are models of $\mathbf{VNC}^1$
by formalizing a proof of Nepomnjascij's Theorem in such cuts. This is a
strengthening of a result by Paris and Wilkie. We can then exploit our result
in Proof Complexity to observe that Frege proof systems can be sub
exponentially simulated by bounded depth Frege proof systems. This result has
recently been obtained by Filmus, Pitassi and Santhanam in a direct proof. As
an interesting observation we also obtain an average case separation of
Resolution from AC0-Frege by applying a recent result with Tzameret.
On (Subgame Perfect) Secure Equilibrium in Quantitative Reachability Games
Authors: Brihaye Thomas , Bruyère Véronique , De Pril Julie , Gimbert Hugo
Published: November 2013

We study turn-based quantitative multiplayer non zero-sum games played on
finite graphs with reachability objectives. In such games, each player aims at
reaching his own goal set of states as soon as possible. A previous work on
this model showed that Nash equilibria (resp. secure equilibria) are guaranteed
to exist in the multiplayer (resp. two-player) case. The existence of secure
equilibria in the multiplayer case remained and is still an open problem. In
this paper, we focus our study on the concept of subgame perfect equilibrium, a
refinement of Nash equilibrium well-suited in the framework of games played on
graphs. We also introduce the new concept of subgame perfect secure
equilibrium. We prove the existence of subgame perfect equilibria (resp.
subgame perfect secure equilibria) in multiplayer (resp. two-player)
quantitative reachability games. Moreover, we provide an algorithm deciding the
existence of secure equilibria in the multiplayer case.
Generalizing determinization from automata to coalgebras
Authors: Silva Alexandra , Bonchi Filippo , Bonsangue Marcello , Rutten Jan
Published: November 2013

The powerset construction is a standard method for converting a
nondeterministic automaton into a deterministic one recognizing the same
language. In this paper, we lift the powerset construction from automata to the
more general framework of coalgebras with structured state spaces. Coalgebra is
an abstract framework for the uniform study of different kinds of dynamical
systems. An endofunctor F determines both the type of systems (F-coalgebras)
and a notion of behavioural equivalence (~_F) amongst them. Many types of
transition systems and their equivalences can be captured by a functor F. For
example, for deterministic automata the derived equivalence is language
equivalence, while for non-deterministic automata it is ordinary bisimilarity.
We give several examples of applications of our generalized determinization
construction, including partial Mealy machines, (structured) Moore automata,
Rabin probabilistic automata, and, somewhat surprisingly, even pushdown
automata. To further witness the generality of the approach we show how to
characterize coalgebraically several equivalences which have been object of
interest in the concurrency community, such as failure or ready semantics.
Decidable Classes of Tree Automata Mixing Local and Global Constraints Modulo Flat Theories
Authors: Barguñó Luis , Creus Carles , Godoy Guillem , Jacquemard Florent , Vacher Camille
Published: November 2013

We define a class of ranked tree automata TABG generalizing both the tree
automata with local tests between brothers of Bogaert and Tison (1992) and with
global equality and disequality constraints (TAGED) of Filiot et al. (2007).
TABG can test for equality and disequality modulo a given flat equational
theory between brother subterms and between subterms whose positions are
defined by the states reached during a computation. In particular, TABG can
check that all the subterms reaching a given state are distinct. This
constraint is related to monadic key constraints for XML documents, meaning
that every two distinct positions of a given type have different values. We
prove decidability of the emptiness problem for TABG. This solves, in
particular, the open question of the decidability of emptiness for TAGED. We
further extend our result by allowing global arithmetic constraints for
counting the number of occurrences of some state or the number of different
equivalence classes of subterms (modulo a given flat equational theory)
reaching some state during a computation. We also adapt the model to unranked
ordered terms. As a consequence of our results for TABG, we prove the
decidability of a fragment of the monadic second order logic on trees extended
with predicates for equality and disequality between subtrees, and cardinality.
Unifying the Linear Time-Branching Time Spectrum of Process Semantics
Authors: Escrig David de Frutos , Gregorio-Rodríguez Carlos , Palomino Miguel , Hernández David Romero
Published: November 2013

Van Glabbeek's linear time-branching time spectrum is one of the most
relevant work on comparative study on process semantics, in which semantics are
partially ordered by their discrimination power. In this paper we bring forward
a refinement of this classification and show how the process semantics can be
dealt with in a uniform way: based on the very natural concept of constrained
simulation we show how we can classify the spectrum in layers; for the families
lying in the same layer we show how to obtain in a generic way equational,
observational, logical and operational characterizations; relations among
layers are also very natural and differences just stem from the constraint
imposed on the simulations that rule the layers. Our methodology also shows how
to achieve a uniform treatment of semantic preorders and equivalences.
Propositional Dynamic Logic with Converse and Repeat for Message-Passing Systems
Authors: Mennicke Roy
Published: November 2013

The model checking problem for propositional dynamic logic (PDL) over message
sequence charts (MSCs) and communicating finite state machines (CFMs) asks,
given a channel bound $B$, a PDL formula $\varphi$ and a CFM $\mathcal{C}$,
whether every existentially $B$-bounded MSC $M$ accepted by $\mathcal{C}$
satisfies $\varphi$. Recently, it was shown that this problem is
PSPACE-complete.
In the present work, we consider CRPDL over MSCs which is PDL equipped with
the operators converse and repeat. The former enables one to walk back and
forth within an MSC using a single path expression whereas the latter allows to
express that a path expression can be repeated infinitely often. To solve the
model checking problem for this logic, we define message sequence chart
automata (MSCAs) which are multi-way alternating parity automata walking on
MSCs. By exploiting a new concept called concatenation states, we are able to
inductively construct, for every CRPDL formula $\varphi$, an MSCA precisely
accepting the set of models of $\varphi$. As a result, we obtain that the model
checking problem for CRPDL and CFMs is still in PSPACE.
Lower Bound on Weights of Large Degree Threshold Functions
Authors: Podolskii Vladimir V.
Published: November 2013

An integer polynomial $p$ of $n$ variables is called a \emph{threshold gate}
for a Boolean function $f$ of $n$ variables if for all $x \in \zoon$ $f(x)=1$
if and only if $p(x)\geq 0$. The \emph{weight} of a threshold gate is the sum
of its absolute values.
In this paper we study how large a weight might be needed if we fix some
function and some threshold degree. We prove $2^{\Omega(2^{2n/5})}$ lower bound
on this value. The best previous bound was $2^{\Omega(2^{n/8})}$ (Podolskii,
2009).
In addition we present substantially simpler proof of the weaker
$2^{\Omega(2^{n/4})}$ lower bound. This proof is conceptually similar to other
proofs of the bounds on weights of nonlinear threshold gates, but avoids a lot
of technical details arising in other proofs. We hope that this proof will help
to show the ideas behind the construction used to prove these lower bounds.
The degree structure of Weihrauch-reducibility
Authors: Higuchi Kojiro , Pauly Arno
Published: November 2013

We answer a question by Vasco Brattka and Guido Gherardi by proving that the
Weihrauch-lattice is not a Brouwer algebra. The computable Weihrauch-lattice is
also not a Heyting algebra, but the continuous Weihrauch-lattice is. We further
investigate the existence of infinite infima and suprema, as well as embeddings
of the Medvedev-degrees into the Weihrauch-degrees.
Two Variable vs. Linear Temporal Logic in Model Checking and Games
Authors: Benedikt Michael , Lenhardt Rastislav , Worrell James
Published: November 2013

Model checking linear-time properties expressed in first-order logic has
non-elementary complexity, and thus various restricted logical languages are
employed. In this paper we consider two such restricted specification logics,
linear temporal logic (LTL) and two-variable first-order logic (FO2). LTL is
more expressive but FO2 can be more succinct, and hence it is not clear which
should be easier to verify. We take a comprehensive look at the issue, giving a
comparison of verification problems for FO2, LTL, and various sublogics thereof
across a wide range of models. In particular, we look at unary temporal logic
(UTL), a subset of LTL that is expressively equivalent to FO2; we also consider
the stutter-free fragment of FO2, obtained by omitting the successor relation,
and the expressively equivalent fragment of UTL, obtained by omitting the next
and previous connectives. We give three logic-to-automata translations which
can be used to give upper bounds for FO2 and UTL and various sublogics. We
apply these to get new bounds for both non-deterministic systems (hierarchical
and recursive state machines, games) and for probabilistic systems (Markov
chains, recursive Markov chains, and Markov decision processes). We couple
these with matching lower-bound arguments. Next, we look at combining FO2
verification techniques with those for LTL. We present here a language that
subsumes both FO2 and LTL, and inherits the model checking properties of both
languages. Our results give both a unified approach to understanding the
behaviour of FO2 and LTL, along with a nearly comprehensive picture of the
complexity of verification for these logics and their sublogics.
Bisimulations Meet PCTL Equivalences for Probabilistic Automata
Authors: Song Lei , Zhang Lijun , Godskesen Jens Chr. , Nielson Flemming
Published: November 2013

Probabilistic automata (PAs) have been successfully applied in formal
verification of concurrent and stochastic systems. Efficient model checking
algorithms have been studied, where the most often used logics for expressing
properties are based on probabilistic computation tree logic (PCTL) and its
extension PCTL^*. Various behavioral equivalences are proposed, as a powerful
tool for abstraction and compositional minimization for PAs. Unfortunately, the
equivalences are well-known to be sound, but not complete with respect to the
logical equivalences induced by PCTL or PCTL*. The desire of a both sound and
complete behavioral equivalence has been pointed out by Segala in 1995, but
remains open throughout the years. In this paper we introduce novel notions of
strong bisimulation relations, which characterize PCTL and PCTL* exactly. We
extend weak bisimulations that characterize PCTL and PCTL* without next
operator, respectively. Further, we also extend the framework to simulation
preorders. Thus, our paper bridges the gap between logical and behavioral
equivalences and preorders in this setting.
Admissibility in Finitely Generated Quasivarieties
Authors: Metcalfe George , Röthlisberger Christoph
Published: November 2013

Checking the admissibility of quasiequations in a finitely generated (i.e.,
generated by a finite set of finite algebras) quasivariety Q amounts to
checking validity in a suitable finite free algebra of the quasivariety, and is
therefore decidable. However, since free algebras may be large even for small
sets of small algebras and very few generators, this naive method for checking
admissibility in $\Q$ is not computationally feasible. In this paper,
algorithms are introduced that generate a minimal (with respect to a multiset
well-ordering on their cardinalities) finite set of algebras such that the
validity of a quasiequation in this set corresponds to admissibility of the
quasiequation in Q. In particular, structural completeness (validity and
admissibility coincide) and almost structural completeness (validity and
admissibility coincide for quasiequations with unifiable premises) can be
checked. The algorithms are illustrated with a selection of well-known finitely
generated quasivarieties, and adapted to handle also admissibility of rules in
finite-valued logics.
Graph Logics with Rational Relations
Authors: Barcelo Pablo , Figueira Diego , Libkin Leonid
Published: November 2013

We investigate some basic questions about the interaction of regular and
rational relations on words. The primary motivation comes from the study of
logics for querying graph topology, which have recently found numerous
applications. Such logics use conditions on paths expressed by regular
languages and relations, but they often need to be extended by rational
relations such as subword or subsequence. Evaluating formulae in such extended
graph logics boils down to checking nonemptiness of the intersection of
rational relations with regular or recognizable relations (or, more generally,
to the generalized intersection problem, asking whether some projections of a
regular relation have a nonempty intersection with a given rational relation).
We prove that for several basic and commonly used rational relations, the
intersection problem with regular relations is either undecidable (e.g., for
subword or su?x, and some generalizations), or decidable with
non-primitive-recursive complexity (e.g., for subsequence and its
generalizations). These results are used to rule out many classes of graph
logics that freely combine regular and rational relations, as well as to
provide the simplest problem related to verifying lossy channel systems that
has non-primitive-recursive complexity. We then prove a dichotomy result for
logics combining regular conditions on individual paths and rational relations
on paths, by showing that the syntactic form of formulae classi?es them into
either e?ciently checkable or undecidable cases. We also give examples of
rational relations for which such logics are decidable even without syntactic
restrictions.
Cartesian closed 2-categories and permutation equivalence in higher-order rewriting
Authors: Hirschowitz Tom
Published: November 2013

We propose a semantics for permutation equivalence in higher-order rewriting.
This semantics takes place in cartesian closed 2-categories, and is proved
sound and complete.
Measure Transformer Semantics for Bayesian Machine Learning
Authors: Borgström Johannes , Gordon Andrew D , Greenberg Michael , Margetson James , Van Gael Jurgen
Published: November 2013

The Bayesian approach to machine learning amounts to computing posterior
distributions of random variables from a probabilistic model of how the
variables are related (that is, a prior distribution) and a set of observations
of variables. There is a trend in machine learning towards expressing Bayesian
models as probabilistic programs. As a foundation for this kind of programming,
we propose a core functional calculus with primitives for sampling prior
distributions and observing variables. We define measure-transformer
combinators inspired by theorems in measure theory, and use these to give a
rigorous semantics to our core calculus. The original features of our semantics
include its support for discrete, continuous, and hybrid measures, and, in
particular, for observations of zero-probability events. We compile our core
language to a small imperative language that is processed by an existing
inference engine for factor graphs, which are data structures that enable many
efficient inference algorithms. This allows efficient approximate inference of
posterior marginal distributions, treating thousands of observations per second
for large instances of realistic models.
Linearizability with Ownership Transfer
Authors: Gotsman Alexey , Yang Hongseok
Published: November 2013

Linearizability is a commonly accepted notion of correctness for libraries of
concurrent algorithms. Unfortunately, it assumes a complete isolation between a
library and its client, with interactions limited to passing values of a given
data type. This is inappropriate for common programming languages, where
libraries and their clients can communicate via the heap, transferring the
ownership of data structures, and can even run in a shared address space
without any memory protection. In this paper, we present the first definition
of linearizability that lifts this limitation and establish an Abstraction
Theorem: while proving a property of a client of a concurrent library, we can
soundly replace the library by its abstract implementation related to the
original one by our generalisation of linearizability. This allows abstracting
from the details of the library implementation while reasoning about the
client. We also prove that linearizability with ownership transfer can be
derived from the classical one if the library does not access some of data
structures transferred to it by the client.
Reachability Problem for Weak Multi-Pushdown Automata
Authors: Czerwiński Wojciech , Hofman Piotr , Lasota SŁawomir
Published: November 2013

This paper is about reachability analysis in a restricted subclass of
multi-pushdown automata. We assume that the control states of an automaton are
partially ordered, and all transitions of an automaton go downwards with
respect to the order. We prove decidability of the reachability problem, and
computability of the backward reachability set. As the main contribution, we
identify relevant subclasses where the reachability problem becomes
NP-complete. This matches the complexity of the same problem for
communication-free vector addition systems, a special case of stateless
multi-pushdown automata.
Pebble Games, Proof Complexity, and Time-Space Trade-offs
Authors: Nordstrom Jakob
Published: November 2013

Pebble games were extensively studied in the 1970s and 1980s in a number of
different contexts. The last decade has seen a revival of interest in pebble
games coming from the field of proof complexity. Pebbling has proven to be a
useful tool for studying resolution-based proof systems when comparing the
strength of different subsystems, showing bounds on proof space, and
establishing size-space trade-offs. This is a survey of research in proof
complexity drawing on results and tools from pebbling, with a focus on proof
space lower bounds and trade-offs between proof size and proof space.
Connector algebras for C/E and P/T nets' interactions
Authors: Bruni Roberto , Melgratti Hernan , Montanari Ugo , Sobocinski Pawel
Published: November 2013

A quite flourishing research thread in the recent literature on
component-based systems is concerned with the algebraic properties of different
classes of connectors. In a recent paper, an algebra of stateless connectors
was presented that consists of five kinds of basic connectors, namely symmetry,
synchronization, mutual exclusion, hiding and inaction, plus their duals, and
it was shown how they can be freely composed in series and in parallel to model
sophisticated 'glues'. In this paper we explore the expressiveness of stateful
connectors obtained by adding one-place buffers or unbounded buffers to the
stateless connectors. The main results are: i) we show how different classes of
connectors exactly correspond to suitable classes of Petri nets equipped with
compositional interfaces, called nets with boundaries; ii) we show that the
difference between strong and weak semantics in stateful connectors is
reflected in the semantics of nets with boundaries by moving from the classic
step semantics (strong case) to a novel banking semantics (weak case), where a
step can be executed by taking some 'debit' tokens to be given back during the
same step; iii) we show that the corresponding bisimilarities are congruences
(w.r.t. composition of connectors in series and in parallel); iv) we show that
suitable monoidality laws, like those arising when representing stateful
connectors in the tile model, can nicely capture concurrency (in the sense of
step semantics) aspects; and v) as a side result, we provide a basic algebra,
with a finite set of symbols, out of which we can compose all P/T nets with
boundaries, fulfilling a long standing quest.
On Characterising Distributability
Authors: van Glabbeek Rob J. , Goltz Ursula , Schicke-Uffmann Jens-Wolfhard
Published: November 2013

We formalise a general concept of distributed systems as sequential
components interacting asynchronously. We define a corresponding class of Petri
nets, called LSGA nets, and precisely characterise those system specifications
which can be implemented as LSGA nets up to branching ST-bisimilarity with
explicit divergence.
Bases as Coalgebras
Authors: Jacobs Bart
Published: November 2013

The free algebra adjunction, between the category of algebras of a monad and
the underlying category, induces a comonad on the category of algebras. The
coalgebras of this comonad are the topic of study in this paper (following
earlier work). It is illustrated how such coalgebras-on-algebras can be
understood as bases, decomposing each element x into primitives elements from
which x can be reconstructed via the operations of the algebra. This holds in
particular for the free vector space monad, but also for other monads, like
powerset or distribution. For instance, continuous dcpos or stably continuous
frames, where each element is the join of the elements way below it, can be
described as such coalgebras. Further, it is shown how these
coalgebras-on-algebras give rise to a comonoid structure for copy and delete,
and thus to diagonalisation of endomaps like in linear algebra.
Unary negation
Authors: Segoufin Luc , Cate Balder ten
Published: November 2013

We study fragments of first-order logic and of least fixed point logic that
allow only unary negation: negation of formulas with at most one free variable.
These logics generalize many interesting known formalisms, including modal
logic and the $\mu$-calculus, as well as conjunctive queries and monadic
Datalog. We show that satisfiability and finite satisfiability are decidable
for both fragments, and we pinpoint the complexity of satisfiability, finite
satisfiability, and model checking. We also show that the unary negation
fragment of first-order logic is model-theoretically very well behaved. In
particular, it enjoys Craig Interpolation and the Projective Beth Property.
Regular Cost Functions, Part I: Logic and Algebra over Words
Authors: Colcombet Thomas
Published: November 2013

The theory of regular cost functions is a quantitative extension to the
classical notion of regularity. A cost function associates to each input a
non-negative integer value (or infinity), as opposed to languages which only
associate to each input the two values "inside" and "outside". This theory is a
continuation of the works on distance automata and similar models. These models
of automata have been successfully used for solving the star-height problem,
the finite power property, the finite substitution problem, the relative
inclusion star-height problem and the boundedness problem for monadic-second
order logic over words. Our notion of regularity can be -- as in the classical
theory of regular languages -- equivalently defined in terms of automata,
expressions, algebraic recognisability, and by a variant of the monadic
second-order logic. These equivalences are strict extensions of the
corresponding classical results. The present paper introduces the cost monadic
logic, the quantitative extension to the notion of monadic second-order logic
we use, and show that some problems of existence of bounds are decidable for
this logic. This is achieved by introducing the corresponding algebraic
formalism: stabilisation monoids.
Computably regular topological spaces
Authors: Weihrauch Klaus
Published: November 2013

This article continues the study of computable elementary topology started by
the author and T. Grubba in 2009 and extends the author's 2010 study of axioms
of computable separation. Several computable T3- and Tychonoff separation
axioms are introduced and their logical relation is investigated. A number of
implications between these axioms are proved and several implications are
excluded by counter examples, however, many questions have not yet been
answered. Known results on computable metrization of T3-spaces from M.
Schr/"oder (1998) and T. Grubba, M. Schr/"oder and the author (2007) are proved
under uniform assumptions and with partly simpler proofs, in particular, the
theorem that every computably regular computable topological space with
non-empty base elements can be embedded into a computable metric space. Most of
the computable separation axioms remain true for finite products of spaces.
Trauma- and Stressor Related Disorders in the Tuareg Refugees of a Camp in Burkina Faso
Authors: Carta M.G. , Oumar F. Wallet , Moro M.F. , Moro D. , Preti A. , Mereu A. , Bhugra D.
Published: November 2013

Background:

Post-traumatic stress disorder (PTSD) is reported to be common among refugees. We set out to explore risk of Trauma- and Stress-or-Related Disorders and the associated burden of psychological distress in a refugee camp of Malian Refugees in Burkina Faso.

Methods:

One out of five persons living in the camp was selected randomly and interviewed using the French version of the Short Screening Scale for PTSD and the validated K6 scale to measure psychiatric morbidity.

Results:

Around 60% of the interviewed sample (N=408) met the criteria for Trauma- and Stress-or-Related Disorders and also reported severe mental distress on K6 scores. Women aged 40 and over were found to be at higher risk of Trauma- and Stress-or-Related Disorders whereas young people (39 or younger) scored higher on K6 ratings. Around 83% of the surveyed subjects had a family member killed in the war, 91% a relative in the war, more than 80% had a family member suffering from physical injuries, and 90% reported problems with food and housing. The frequency of these life events was not surprisingly higher in persons with Trauma- and Stress-or-Related Disorders, with the death of a family member and severe problems with food being specifically related to them.Conclusion: These results point to important psychological suffering in a population that is often ignored by the media and international political authorities. Immediate steps are required to provide urgent legal and humanitarian protection to those who are forced to flee their homes and cross international borders because of disasters.
Preoperative Digital Carotid Compression as a Predictor of the Need for Shunting During Carotid Endarterectomy
Authors: Naraynsingh Vijay , Harnarayan Patrick , Maharaj Ravi , Dan Dilip , Hariharan Seetharaman
Published: November 2013

This study prospectively attempted to assess the need for shunting by preoperative digital compression of the proximal common carotid artery and correlated these findings with intraoperative assessment while performing carotid endarterectomy under local anaesthesia. Preoperative digital compression is highly predictive of the need for shunting intra-operatively and can be used as a valuable test in carefully chosen patients. This may help in decreasing the need for advanced neurological monitoring during carotid endarterectomy.
Type of Valvular Heart Disease Requiring Surgery in the 21st Century: Mortality and Length-of-Stay Related to Surgery
Authors: Boudoulas Konstantinos Dean , Ravi Yazhini , Garcia Daniel , Saini Uksha , Sofowora Gbemiga G. , Gumina Richard J. , Sai-Sudhakar Chittoor B.
Published: November 2013

Aim:

While the incidence of rheumatic heart disease has declined dramatically over the last half-century, the number of valve surgeries has not changed. This study was undertaken to define the most common type of valvular heart disease requiring surgery today, and determine in-hospital surgical mortality and length-of-stay (LOS) for isolated aortic or mitral valve surgery in a United States tertiary-care hospital.

Methods:

Patients with valve surgery between January 2002 to June 2008 at The Ohio State University Medical Center were studied. Patients only with isolated aortic or mitral valve surgery were analyzed.

Results:

From 915 patients undergoing at least aortic or mitral valve surgery, the majority had concomitant cardiac proce-dures mostly coronary artery bypass grafting (CABG); only 340 patients had isolated aortic (n=204) or mitral (n=136) valve surgery. In-hospital surgical mortality for mitral regurgitation (n=119), aortic stenosis (n=151), aortic insufficiency (n=53) and mitral stenosis (n=17) was 2.5% (replacement 3.4%; repair 1.6%), 3.9%, 5.6% and 5.8%, respectively (p=NS). Median LOS for aortic insufficiency, aortic stenosis, mitral regurgitation, and mitral stenosis was 7, 8, 9 (replacement 11.5; repair 7) and 11 days, respectively (p<0.05 for group). In-hospital surgical mortality for single valve surgery plus CABG was 10.2% (p<0.005 compared to single valve surgery).

Conclusions:

Aortic stenosis and mitral regurgitation are the most common valvular lesions requiring surgery today. Surgery for isolated aortic or mitral valve disease has low in-hospital mortality with modest LOS. Concomitant CABG with valve surgery increases mortality substantially. Hospital analysis is needed to monitor quality and stimulate improvement among Institutions.
A Keratocyst in the Buccal Mucosa with the Features of Keratocystic Odontogenic Tumor
Authors: Yamamoto Kazuhiko , Matsusue Yumiko , Kurihara Miyako , Takahashi Yuka , Kirita Tadaaki
Published: November 2013

A 74-year-old male patient consulted us for an elastic firm mass in the right buccal mucosa. CT examination revealed a well-circumscribed oval cystic lesion in the anterior region of the masseter muscle. On MRI, the lesion showed a low signal on T1-weighted image and a high signal on T2-weighted image. Aspiration biopsy demonstrated the presence of squamous cells in whitish liquid. Under the diagnosis of epidermoid cyst, the lesion was intraorally extirpated under general anesthesia. The lesion was cystic at the size of 30 × 25mm. Histologically, the cyst wall was lined with parakeratinized squamous epithelium corrugated on its surface, the basal layer of which consisted of cuboidal cells showing palisading of the nuclei. Immunohistochemically, the lining epithelium was positive for CK17 and negative for CK10. The basal and suprabasal cells were labeled for Ki-67 at a relatively high rate. These features are compatible with those of keratocystic odontogenic tumor.
Use of external Indicators to Evaluate Stress of Largemouth (Micropterus
salmoides) and Smallmouth (M. dolomieu) Bass at Tournaments
Authors: Maynard George A. , Mihuc Timothy B. , Schultz Rachel E. , Sotola V. Alex , Reyes Alejandro J. , Malchoff Mark H. , Garneau Danielle E.
Published: November 2013

The popularity of catch and release tournaments targeting largemouth (Micropterus
salmoides) and smallmouth
(M. dolomieu) bass has continued to increase over the past few decades. In 2008, Lake Champlain hosted 95 tournaments,
including several large-scale events hosted in Plattsburgh, NY. As in any catch-and-release fishery, released fish exhibit
varying amounts and types of stress, potentially generating sub-lethal population-level impacts. Due to the large volume
of fish that move through catch and release tournaments, blood chemistry analysis is generally outside of the temporal and
financial constraints of tournament organizers. External indicators of stress can be used to determine stress levels in large
numbers of fish. We adapted some of these indicators (e.g., wounding, response to stimuli) from research in marine and
commercial fisheries to assess fish stress following weigh-in at Plattsburgh-based catch and release tournaments. Additionally,
we collected data including fish measurements, lake temperature, fish capture locations, and information on tournament
handling practices to determine which external factors influenced fish stress levels. Generalized linear models
showed increased likelihood of elevated stress levels as a positive function of ambient lake temperature, fish size, and
livewell transport distance. Comparison of results with existing research on bass stress are consistent with our models, indicating
that external signs of stress can be used to evaluate black bass stress levels at catch-and-release tournaments.
EDITORIAL: No-Pharmacological Intervention: Pomegranate Juice for the Management
of Hypertension and the Improvement of Cardiovascular Health
Authors: Tziomalos Konstantinos , Doumas Michael , Athyros Vasilios G.
Published: November 2013

Full text available.
LETTER TO THE EDITOR: Pomegranate Juice Intake and Cardiovascular Health
Authors: Notara Venetia , Panagiotakos Demosthenes B.
Published: November 2013

The public health burden of cardiovascular diseases
(CVDs) is substantial. According to the World Health Organization
report “The Global Burden of Disease” 2013 Update,
heart diseases are expected to take the second place in
the rank order of disease and injury burden by the year 2030
[1]. More than 50% reduction of CVD mortality is attributable
to favourable changes in risk factors, while 43% to new
medical and surgical treatment [2,3]. Extended research data
has indicated that diet is one of the modifiable risk factors
that has been substantially related to CVD prevention,
through several serum antioxidant and antithrombotic
mechanisms. Emphasis has been given to the daily consumption
of fruits and vegetables due to the high source, among
others, of phenolic acids and flavonoids that are known for
their antioxidant properties [4]. In the most recent years,
laboratory and clinical studies have examined the health
benefits of pomegranate juice consumption, which have
demonstrated its protective effect against the progression of
atherosclerosis [5]. Pomegranate fruit has very high levels of
antioxidants- mainly polyphenols- as well as tannins and
anthocyanins, which seem to improve vascular function and
modulation of inflammation. In a recent study conducted in a
sample of people with hypertension, it has been observed
that pomegranate juice can significantly lower blood pressure
even in a 2-week intake of fresh juice [6]. Polyphenolic
flavonoids are powerful antioxidants which can inhibit the
harmful oxidation effect of low-density LDL and consequently
restrain atherosclerosis development [7]. Pomegranate
seed oil consumption seems to be associated with an improvement
in insulin sensitivity, posing an additional protective
effect in the development of type 2 diabetes [8]. However,
in the same study the CVD – related risk did not
change, while other studies did not show a decrease in the
type 2 diabetes risk or a reduction in the lipid peroxidation
among healthy controls, too [5,9]. It should also be mentioned,
that pomegranate seed oil does not have polyhpenols.

Despite the fact that dietary flavonoids seem to have a
potential effect on the reduction of CVD risk, the question of
whether isolated polyphenols are the responsible compounds
for vascular health still remains unanswered. Long-term
clinical studies exploring the bioactive compounds of various
types of fruits are required to determine the potential synergistic
effects of polyphenols and the dose-response relationships
[10]. Additionally, the impact of pomegranate polyphenol
extracts among healthy and high CVD risk subjects
needs further investigation.
LETTER TO THE EDITOR: Do we Need Functional Foods for the Treatment of Hypertension?
Authors: Mitsiou Evdoxia K.
Published: November 2013

I read with interest the Editorial by Dr. Tziomalos et al
[1]. The use of "alternative" treatments or functional
foods/beverages for the treatment of arterial hypertension is
getting increasingly prevalent. The paper is in this direction,
supporting this trend. However, there are some issues that
might be related to the use of such treatment modalities.

First, is it possible that the use of pomegranate juice (PJ),
a functional beverage, will reduce the adherence of hypertensive
to the antihypertensive drug treatment that they might
need for the effective control of their blood pressure? It has
been shown that the use of functional foods or dietary supplements
may offer opportunities to reduce health risk factors
and risk of diseases, both as monotherapy and in combination
with prescription drugs. Nevertheless, the potential
caveats or false claims of these products should not be overlooked
[2]. Should we jeopardize the necessary drug treatment
for a functional food?

Second, authors mention that one of the mechanisms of
action of PJ is angiotensin converting enzyme (ACE) inhibition.
In a short term (4 weeks) study, results showed that PJ
reduced blood pressure (BP), however the fall in BP was not
paralleled by changes in concentration of serum ACE [3].

Third, in the case that PJ indeed reduces ACE activity,
would PJ administration be equally effective if coadministered
with an ACE inhibitor or should we avoid such
a co-administration?

Fourth, do authors consider that the use of PJ indeed improved
CV health of hypertensives that they use it and if yes
why?

It would be interesting and useful if these issues were
sorted out.