### A concurrency control problem in a time-sharing system with different job types

Skip to main content (access key 's'),
Skip to navigation (access key 'n'),
Accessibility information (access key '0')

An illustration of coinduction in terms of a notion of weak bisimilarity is presented. First, an operational semantics $\mathcal{O}$ for while programs is defined in terms of a final automaton. It identifies any two programs that are weakly bisimilar, and induces in a canonical manner a compositional model $\mathcal{D}$. Next $\mathcal{O}=\mathcal{D}$ is proved by coinduction.

This survey presents major results and issues related to the study of NPO problems in dynamic environments, that is, in settings where instances are allowed to undergo some modifications over time. In particular, the survey focuses on two complementary frameworks. The first one is the reoptimization framework, where an instance I that is already solved undergoes some local perturbation. The goal is then to make use of the information provided by the initial solution to compute a new solution. The...

This paper describes a modification of the power set construction for the transformation of self-verifying nondeterministic finite automata to deterministic ones. Using a set counting argument, the upper bound for this transformation can be lowered from ${2}^{n}$ to $O\left(\frac{{2}^{n}}{\sqrt{n}}\right).$

We introduce and investigate Nondeterministically Bounded Modulo Counter Automata (NBMCA), which are two-way multi-head automata that comprise a constant number of modulo counters, where the counter bounds are nondeterministically guessed, and this is the only element of nondeterminism. NBMCA are tailored to recognising those languages that are characterised by the existence of a specific factorisation of their words, e. g., pattern languages. In this work, we subject NBMCA to a theoretically sound...

Real functions on the domain ${[0,1)}^{n}$ – often used to describe digital images – allow for different well-known types of binary operations. In this note, we recapitulate how weighted finite automata can be used in order to represent those functions and how certain binary operations are reflected in the theory of these automata. Different types of products of automata are employed, including the seldomly-used full cartesian product. We show, however, the infeasibility of functional composition; simple examples...

Real functions on the domain [0,1)n – often used to describe digital images – allow for different well-known types of binary operations. In this note, we recapitulate how weighted finite automata can be used in order to represent those functions and how certain binary operations are reflected in the theory of these automata. Different types of products of automata are employed, including the seldomly-used full Cartesian product. We show, however, the infeasibility of functional composition; simple...

More than a decade ago, Moller and Tofts published their seminal work on relating processes, which are annotated with lower time bounds, with respect to speed. Their paper has left open many questions regarding the semantic theory for the suggested bisimulation-based faster-than preorder, the MT-preorder, which have not been addressed since. The encountered difficulties concern a general compositionality result, a complete axiom system for finite processes, a convincing intuitive justification of...

More than a decade ago, Moller and Tofts published their seminal work on relating processes, which are annotated with lower time bounds, with respect to speed. Their paper has left open many questions regarding the semantic theory for the suggested bisimulation-based faster-than preorder, the MT-preorder, which have not been addressed since. The encountered difficulties concern a general compositionality result, a complete axiom system for finite processes, a convincing intuitive justification...

This paper offers characteristic formula constructions in the real-time logic Lν for several behavioural relations between (states of) timed automata. The behavioural relations studied in this work are timed (bi)similarity, timed ready simulation, faster-than bisimilarity and timed trace inclusion. The characteristic formulae delivered by our constructions have size which is linear in that of the timed automaton they logically describe. This also applies to the characteristic formula for...

We investigate well-structured graph-driven parity-FBDDs, which strictly generalize the two well-known models parity OBDDs and well-structured graph-driven FBDDs. The first main result is a characterization of the complexity of Boolean functions represented by well-structured graph-driven parity-FBDDs in terms of invariants of the function represented and the graph-ordering used. As a consequence, we derive a lower bound criterion and prove an exponential lower bound for certain linear code functions....

We investigate well-structured graph-driven parity-FBDDs, which strictly generalize the two well-known models parity OBDDs and well-structured graph-driven FBDDs. The first main result is a characterization of the complexity of Boolean functions represented by well-structured graph-driven parity-FBDDs in terms of invariants of the function represented and the graph-ordering used. As a consequence, we derive a lower bound criterion and prove an exponential lower bound for certain linear code functions. The...