@inproceedings{1374, abstract = {We study two-player zero-sum games over infinite-state graphs equipped with ωB and finitary conditions. Our first contribution is about the strategy complexity, i.e the memory required for winning strategies: we prove that over general infinite-state graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory suffices for finitary parity games. We then study pushdown games with boundedness conditions, with two contributions. First we prove a collapse result for pushdown games with ωB-conditions, implying the decidability of solving these games. Second we consider pushdown games with finitary parity along with stack boundedness conditions, and show that solving these games is EXPTIME-complete.}, author = {Chatterjee, Krishnendu and Fijalkow, Nathanaël}, booktitle = {22nd EACSL Annual Conference on Computer Science Logic}, location = {Torino, Italy}, pages = {181 -- 196}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Infinite-state games with finitary conditions}}, doi = {10.4230/LIPIcs.CSL.2013.181}, volume = {23}, year = {2013}, } @inproceedings{1376, abstract = {We consider the distributed synthesis problem for temporal logic specifications. Traditionally, the problem has been studied for LTL, and the previous results show that the problem is decidable iff there is no information fork in the architecture. We consider the problem for fragments of LTL and our main results are as follows: (1) We show that the problem is undecidable for architectures with information forks even for the fragment of LTL with temporal operators restricted to next and eventually. (2) For specifications restricted to globally along with non-nested next operators, we establish decidability (in EXPSPACE) for star architectures where the processes receive disjoint inputs, whereas we establish undecidability for architectures containing an information fork-meet structure. (3) Finally, we consider LTL without the next operator, and establish decidability (NEXPTIME-complete) for all architectures for a fragment that consists of a set of safety assumptions, and a set of guarantees where each guarantee is a safety, reachability, or liveness condition.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan and Pavlogiannis, Andreas}, booktitle = {13th International Conference on Formal Methods in Computer-Aided Design}, location = {Portland, OR, United States}, pages = {18 -- 25}, publisher = {IEEE}, title = {{Distributed synthesis for LTL fragments}}, doi = {10.1109/FMCAD.2013.6679386}, year = {2013}, } @inproceedings{1385, abstract = {It is often difficult to correctly implement a Boolean controller for a complex system, especially when concurrency is involved. Yet, it may be easy to formally specify a controller. For instance, for a pipelined processor it suffices to state that the visible behavior of the pipelined system should be identical to a non-pipelined reference system (Burch-Dill paradigm). We present a novel procedure to efficiently synthesize multiple Boolean control signals from a specification given as a quantified first-order formula (with a specific quantifier structure). Our approach uses uninterpreted functions to abstract details of the design. We construct an unsatisfiable SMT formula from the given specification. Then, from just one proof of unsatisfiability, we use a variant of Craig interpolation to compute multiple coordinated interpolants that implement the Boolean control signals. Our method avoids iterative learning and back-substitution of the control functions. We applied our approach to synthesize a controller for a simple two-stage pipelined processor, and present first experimental results.}, author = {Hofferek, Georg and Gupta, Ashutosh and Könighofer, Bettina and Jiang, Jie and Bloem, Roderick}, booktitle = {2013 Formal Methods in Computer-Aided Design}, location = {Portland, OR, United States}, pages = {77 -- 84}, publisher = {IEEE}, title = {{Synthesizing multiple boolean functions using interpolation on a single proof}}, doi = {10.1109/FMCAD.2013.6679394}, year = {2013}, } @inproceedings{1387, abstract = {Choices made by nondeterministic word automata depend on both the past (the prefix of the word read so far) and the future (the suffix yet to be read). In several applications, most notably synthesis, the future is diverse or unknown, leading to algorithms that are based on deterministic automata. Hoping to retain some of the advantages of nondeterministic automata, researchers have studied restricted classes of nondeterministic automata. Three such classes are nondeterministic automata that are good for trees (GFT; i.e., ones that can be expanded to tree automata accepting the derived tree languages, thus whose choices should satisfy diverse futures), good for games (GFG; i.e., ones whose choices depend only on the past), and determinizable by pruning (DBP; i.e., ones that embody equivalent deterministic automata). The theoretical properties and relative merits of the different classes are still open, having vagueness on whether they really differ from deterministic automata. In particular, while DBP ⊆ GFG ⊆ GFT, it is not known whether every GFT automaton is GFG and whether every GFG automaton is DBP. Also open is the possible succinctness of GFG and GFT automata compared to deterministic automata. We study these problems for ω-regular automata with all common acceptance conditions. We show that GFT=GFG⊃DBP, and describe a determinization construction for GFG automata.}, author = {Boker, Udi and Kuperberg, Denis and Kupferman, Orna and Skrzypczak, Michał}, location = {Riga, Latvia}, number = {PART 2}, pages = {89 -- 100}, publisher = {Springer}, title = {{Nondeterminism in the presence of a diverse or unknown future}}, doi = {10.1007/978-3-642-39212-2_11}, volume = {7966}, year = {2013}, } @phdthesis{1405, abstract = {Motivated by the analysis of highly dynamic message-passing systems, i.e. unbounded thread creation, mobility, etc. we present a framework for the analysis of depth-bounded systems. Depth-bounded systems are one of the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. Even though they are infinite state systems depth-bounded systems are well-structured, thus can be analyzed algorithmically. We give an interpretation of depth-bounded systems as graph-rewriting systems. This gives more flexibility and ease of use to apply depth-bounded systems to other type of systems like shared memory concurrency. First, we develop an adequate domain of limits for depth-bounded systems, a prerequisite for the effective representation of downward-closed sets. Downward-closed sets are needed by forward saturation-based algorithms to represent potentially infinite sets of states. Then, we present an abstract interpretation framework to compute the covering set of well-structured transition systems. Because, in general, the covering set is not computable, our abstraction over-approximates the actual covering set. Our abstraction captures the essence of acceleration based-algorithms while giving up enough precision to ensure convergence. We have implemented the analysis in the PICASSO tool and show that it is accurate in practice. Finally, we build some further analyses like termination using the covering set as starting point.}, author = {Zufferey, Damien}, issn = {2663-337X}, pages = {134}, publisher = {Institute of Science and Technology Austria}, title = {{Analysis of dynamic message passing programs}}, doi = {10.15479/at:ista:1405}, year = {2013}, } @phdthesis{1406, abstract = {Epithelial spreading is a critical part of various developmental and wound repair processes. Here we use zebrafish epiboly as a model system to study the cellular and molecular mechanisms underlying the spreading of epithelial sheets. During zebrafish epiboly the enveloping cell layer (EVL), a simple squamous epithelium, spreads over the embryo to eventually cover the entire yolk cell by the end of gastrulation. The EVL leading edge is anchored through tight junctions to the yolk syncytial layer (YSL), where directly adjacent to the EVL margin a contractile actomyosin ring is formed that is thought to drive EVL epiboly. The prevalent view in the field was that the contractile ring exerts a pulling force on the EVL margin, which pulls the EVL towards the vegetal pole. However, how this force is generated and how it affects EVL morphology still remains elusive. Moreover, the cellular mechanisms mediating the increase in EVL surface area, while maintaining tissue integrity and function are still unclear. Here we show that the YSL actomyosin ring pulls on the EVL margin by two distinct force-generating mechanisms. One mechanism is based on contraction of the ring around its circumference, as previously proposed. The second mechanism is based on actomyosin retrogade flows, generating force through resistance against the substrate. The latter can function at any epiboly stage even in situations where the contraction-based mechanism is unproductive. Additionally, we demonstrate that during epiboly the EVL is subjected to anisotropic tension, which guides the orientation of EVL cell division along the main axis (animal-vegetal) of tension. The influence of tension in cell division orientation involves cell elongation and requires myosin-2 activity for proper spindle alignment. Strikingly, we reveal that tension-oriented cell divisions release anisotropic tension within the EVL and that in the absence of such divisions, EVL cells undergo ectopic fusions. We conclude that forces applied to the EVL by the action of the YSL actomyosin ring generate a tension anisotropy in the EVL that orients cell divisions, which in turn limit tissue tension increase thereby facilitating tissue spreading.}, author = {Campinho, Pedro}, issn = {2663-337X}, pages = {123}, publisher = {Institute of Science and Technology Austria}, title = {{Mechanics of zebrafish epiboly: Tension-oriented cell divisions limit anisotropic tissue tension in epithelial spreading}}, year = {2013}, } @article{9459, abstract = {Nucleosome remodelers of the DDM1/Lsh family are required for DNA methylation of transposable elements, but the reason for this is unknown. How DDM1 interacts with other methylation pathways, such as small-RNA-directed DNA methylation (RdDM), which is thought to mediate plant asymmetric methylation through DRM enzymes, is also unclear. Here, we show that most asymmetric methylation is facilitated by DDM1 and mediated by the methyltransferase CMT2 separately from RdDM. We find that heterochromatic sequences preferentially require DDM1 for DNA methylation and that this preference depends on linker histone H1. RdDM is instead inhibited by heterochromatin and absolutely requires the nucleosome remodeler DRD1. Together, DDM1 and RdDM mediate nearly all transposon methylation and collaborate to repress transposition and regulate the methylation and expression of genes. Our results indicate that DDM1 provides DNA methyltransferases access to H1-containing heterochromatin to allow stable silencing of transposable elements in cooperation with the RdDM pathway.}, author = {Zemach, Assaf and Kim, M. Yvonne and Hsieh, Ping-Hung and Coleman-Derr, Devin and Eshed-Williams, Leor and Thao, Ka and Harmer, Stacey L. and Zilberman, Daniel}, issn = {1097-4172}, journal = {Cell}, number = {1}, pages = {193--205}, publisher = {Elsevier}, title = {{The Arabidopsis nucleosome remodeler DDM1 allows DNA methyltransferases to access H1-containing heterochromatin}}, doi = {10.1016/j.cell.2013.02.033}, volume = {153}, year = {2013}, } @article{9481, abstract = {Arabidopsis thaliana endosperm, a transient tissue that nourishes the embryo, exhibits extensive localized DNA demethylation on maternally inherited chromosomes. Demethylation mediates parent-of-origin–specific (imprinted) gene expression but is apparently unnecessary for the extensive accumulation of maternally biased small RNA (sRNA) molecules detected in seeds. Endosperm DNA in the distantly related monocots rice and maize is likewise locally hypomethylated, but whether this hypomethylation is generally parent-of-origin specific is unknown. Imprinted expression of sRNA also remains uninvestigated in monocot seeds. Here, we report high-coverage sequencing of the Kitaake rice cultivar that enabled us to show that localized hypomethylation in rice endosperm occurs solely on the maternal genome, preferring regions of high DNA accessibility. Maternally expressed imprinted genes are enriched for hypomethylation at putative promoter regions and transcriptional termini and paternally expressed genes at promoters and gene bodies, mirroring our recent results in A. thaliana. However, unlike in A. thaliana, rice endosperm sRNA populations are dominated by specific strong sRNA-producing loci, and imprinted 24-nt sRNAs are expressed from both parental genomes and correlate with hypomethylation. Overlaps between imprinted sRNA loci and imprinted genes expressed from opposite alleles suggest that sRNAs may regulate genomic imprinting. Whereas sRNAs in seedling tissues primarily originate from small class II (cut-and-paste) transposable elements, those in endosperm are more uniformly derived, including sequences from other transposon classes, as well as genic and intergenic regions. Our data indicate that the endosperm exhibits a unique pattern of sRNA expression and suggest that localized hypomethylation of maternal endosperm DNA is conserved in flowering plants.}, author = {Rodrigues, Jessica A. and Ruan, Randy and Nishimura, Toshiro and Sharma, Manoj K. and Sharma, Rita and Ronald, Pamela C and Fischer, Robert L. and Zilberman, Daniel}, issn = {1091-6490}, journal = {Proceedings of the National Academy of Sciences}, keywords = {Multidisciplinary}, number = {19}, pages = {7934--7939}, publisher = {National Academy of Sciences}, title = {{Imprinted expression of genes and small RNA is associated with localized hypomethylation of the maternal genome in rice endosperm}}, doi = {10.1073/pnas.1306164110}, volume = {110}, year = {2013}, } @article{9520, abstract = {Plants undergo alternation of generation in which reproductive cells develop in the plant body ("sporophytic generation") and then differentiate into a multicellular gamete-forming "gametophytic generation." Different populations of helper cells assist in this transgenerational journey, with somatic tissues supporting early development and single nurse cells supporting gametogenesis. New data reveal a two-way relationship between early reproductive cells and their helpers involving complex epigenetic and signaling networks determining cell number and fate. Later, the egg cell plays a central role in specifying accessory cells, whereas in both gametophytes, companion cells contribute non-cell-autonomously to the epigenetic landscape of the gamete genomes.}, author = {Feng, Xiaoqi and Zilberman, Daniel and Dickinson, Hugh}, issn = {1878-1551}, journal = {Developmental Cell}, number = {3}, pages = {215--225}, publisher = {Elsevier}, title = {{A conversation across generations: Soma-germ cell crosstalk in plants}}, doi = {10.1016/j.devcel.2013.01.014}, volume = {24}, year = {2013}, } @article{10396, abstract = {Stimfit is a free cross-platform software package for viewing and analyzing electrophysiological data. It supports most standard file types for cellular neurophysiology and other biomedical formats. Its analysis algorithms have been used and validated in several experimental laboratories. Its embedded Python scripting interface makes Stimfit highly extensible and customizable.}, author = {Schlögl, Alois and Jonas, Peter M and Schmidt-Hieber, C. and Guzman, S. J.}, issn = {1862-278X}, journal = {Biomedical Engineering / Biomedizinische Technik}, keywords = {biomedical engineering, data analysis, free software}, location = {Graz, Austria}, number = {SI-1-Track-G}, publisher = {De Gruyter}, title = {{Stimfit: A fast visualization and analysis environment for cellular neurophysiology}}, doi = {10.1515/bmt-2013-4181}, volume = {58}, year = {2013}, } @misc{9749, abstract = {Cooperative behavior, where one individual incurs a cost to help another, is a wide spread phenomenon. Here we study direct reciprocity in the context of the alternating Prisoner's Dilemma. We consider all strategies that can be implemented by one and two-state automata. We calculate the payoff matrix of all pairwise encounters in the presence of noise. We explore deterministic selection dynamics with and without mutation. Using different error rates and payoff values, we observe convergence to a small number of distinct equilibria. Two of them are uncooperative strict Nash equilibria representing always-defect (ALLD) and Grim. The third equilibrium is mixed and represents a cooperative alliance of several strategies, dominated by a strategy which we call Forgiver. Forgiver cooperates whenever the opponent has cooperated; it defects once when the opponent has defected, but subsequently Forgiver attempts to re-establish cooperation even if the opponent has defected again. Forgiver is not an evolutionarily stable strategy, but the alliance, which it rules, is asymptotically stable. For a wide range of parameter values the most commonly observed outcome is convergence to the mixed equilibrium, dominated by Forgiver. Our results show that although forgiving might incur a short-term loss it can lead to a long-term gain. Forgiveness facilitates stable cooperation in the presence of exploitation and noise.}, author = {Zagorsky, Benjamin and Reiter, Johannes and Chatterjee, Krishnendu and Nowak, Martin}, publisher = {Public Library of Science}, title = {{Forgiver triumphs in alternating prisoner's dilemma }}, doi = {10.1371/journal.pone.0080814.s001}, year = {2013}, } @misc{9751, abstract = {High relatedness among interacting individuals has generally been considered a precondition for the evolution of altruism. However, kin-selection theory also predicts the evolution of altruism when relatedness is low, as long as the cost of the altruistic act is minor compared to its benefit. Here, we demonstrate evidence for a low-cost altruistic act in bacteria. We investigated Escherichia coli responding to the attack of an obligately lytic phage by committing suicide in order to prevent parasite transmission to nearby relatives. We found that bacterial suicide provides large benefits to survivors at marginal costs to committers. The cost of suicide was low because infected cells are moribund, rapidly dying upon phage infection, such that no more opportunity for reproduction remains. As a consequence of its marginal cost, host suicide was selectively favoured even when relatedness between committers and survivors approached zero. Altogether, our findings demonstrate that low-cost suicide can evolve with ease, represents an effective host-defence strategy, and seems to be widespread among microbes. Moreover, low-cost suicide might also occur in higher organisms as exemplified by infected social insect workers leaving the colony to die in isolation.}, author = {Refardt, Dominik and Bergmiller, Tobias and Kümmerli, Rolf}, publisher = {Dryad}, title = {{Data from: Altruism can evolve when relatedness is low: evidence from bacteria committing suicide upon phage infection}}, doi = {10.5061/dryad.b1q2n}, year = {2013}, } @misc{9754, abstract = {Short-read sequencing technologies have in principle made it feasible to draw detailed inferences about the recent history of any organism. In practice, however, this remains challenging due to the difficulty of genome assembly in most organisms and the lack of statistical methods powerful enough to discriminate among recent, non-equilibrium histories. We address both the assembly and inference challenges. We develop a bioinformatic pipeline for generating outgroup-rooted alignments of orthologous sequence blocks from de novo low-coverage short-read data for a small number of genomes, and show how such sequence blocks can be used to fit explicit models of population divergence and admixture in a likelihood framework. To illustrate our approach, we reconstruct the Pleistocene history of an oak-feeding insect (the oak gallwasp Biorhiza pallida) which, in common with many other taxa, was restricted during Pleistocene ice ages to a longitudinal series of southern refugia spanning theWestern Palaearctic. Our analysis of sequence blocks sampled from a single genome from each of three major glacial refugia reveals support for an unexpected history dominated by recent admixture. Despite the fact that 80% of the genome is affected by admixture during the last glacial cycle, we are able to infer the deeper divergence history of these populations. These inferences are robust to variation in block length, mutation model, and the sampling location of individual genomes within refugia. This combination of de novo assembly and numerical likelihood calculation provides a powerful framework for estimating recent population history that can be applied to any organism without the need for prior genetic resources.}, author = {Hearn, Jack and Stone, Graham and Barton, Nicholas H and Lohse, Konrad and Bunnefeld, Lynsey}, publisher = {Dryad}, title = {{Data from: Likelihood-based inference of population history from low coverage de novo genome assemblies}}, doi = {10.5061/dryad.r3r60}, year = {2013}, } @article{450, abstract = {Understanding the relative importance of heterosis and outbreeding depression over multiple generations is a key question in evolutionary biology and is essential for identifying appropriate genetic sources for population and ecosystem restoration. Here we use 2455 experimental crosses between 12 population pairs of the rare perennial plant Rutidosis leptorrhynchoides (Asteraceae) to investigate the multi-generational (F1, F2, F3) fitness outcomes of inter-population hybridization. We detected no evidence of outbreeding depression, with inter-population hybrids and backcrosses showing either similar fitness or significant heterosis for fitness components across the three generations. Variation in heterosis among population pairs was best explained by characteristics of the foreign source or home population, and was greatest when the source population was large, with high genetic diversity and low inbreeding, and the home population was small and inbred. Our results indicate that the primary consideration for maximizing progeny fitness following population augmentation or restoration is the use of seed from large, genetically diverse populations.}, author = {Pickup, Melinda and Field, David and Rowell, David and Young, Andrew}, journal = {Proceedings of the Royal Society of London Series B Biological Sciences}, number = {1750}, publisher = {Royal Society, The}, title = {{Source population characteristics affect heterosis following genetic rescue of fragmented plant populations}}, doi = {10.1098/rspb.2012.2058}, volume = {280}, year = {2013}, } @inproceedings{2715, abstract = {We consider Markov decision processes (MDPs) with specifications given as Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning vertices from where the objective can be ensured with probability 1. We study for the first time the average case complexity of the classical algorithm for computing the set of almost-sure winning vertices for MDPs with Büchi objectives. Our contributions are as follows: First, we show that for MDPs with constant out-degree the expected number of iterations is at most logarithmic and the average case running time is linear (as compared to the worst case linear number of iterations and quadratic time complexity). Second, for the average case analysis over all MDPs we show that the expected number of iterations is constant and the average case running time is linear (again as compared to the worst case linear number of iterations and quadratic time complexity). Finally we also show that given that all MDPs are equally likely, the probability that the classical algorithm requires more than constant number of iterations is exponentially small.}, author = {Chatterjee, Krishnendu and Joglekar, Manas and Shah, Nisarg}, location = {Hyderabad, India}, pages = {461 -- 473}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives}}, doi = {10.4230/LIPIcs.FSTTCS.2012.461}, volume = {18}, year = {2012}, } @inproceedings{2825, abstract = {We study the problem of maximum marginal prediction (MMP) in probabilistic graphical models, a task that occurs, for example, as the Bayes optimal decision rule under a Hamming loss. MMP is typically performed as a two-stage procedure: one estimates each variable's marginal probability and then forms a prediction from the states of maximal probability. In this work we propose a simple yet effective technique for accelerating MMP when inference is sampling-based: instead of the above two-stage procedure we directly estimate the posterior probability of each decision variable. This allows us to identify the point of time when we are sufficiently certain about any individual decision. Whenever this is the case, we dynamically prune the variables we are confident about from the underlying factor graph. Consequently, at any time only samples of variables whose decision is still uncertain need to be created. Experiments in two prototypical scenarios, multi-label classification and image inpainting, show that adaptive sampling can drastically accelerate MMP without sacrificing prediction accuracy.}, author = {Lampert, Christoph}, location = {Lake Tahoe, NV, United States}, pages = {82 -- 90}, publisher = {Neural Information Processing Systems}, title = {{Dynamic pruning of factor graphs for maximum marginal prediction}}, volume = {1}, year = {2012}, } @article{2848, abstract = {We study evolutionary game theory in a setting where individuals learn from each other. We extend the traditional approach by assuming that a population contains individuals with different learning abilities. In particular, we explore the situation where individuals have different search spaces, when attempting to learn the strategies of others. The search space of an individual specifies the set of strategies learnable by that individual. The search space is genetically given and does not change under social evolutionary dynamics. We introduce a general framework and study a specific example in the context of direct reciprocity. For this example, we obtain the counter intuitive result that cooperation can only evolve for intermediate benefit-to-cost ratios, while small and large benefit-to-cost ratios favor defection. Our paper is a step toward making a connection between computational learning theory and evolutionary game dynamics.}, author = {Chatterjee, Krishnendu and Zufferey, Damien and Nowak, Martin}, journal = {Journal of Theoretical Biology}, pages = {161 -- 173}, publisher = {Elsevier}, title = {{Evolutionary game dynamics in populations with different learners}}, doi = {10.1016/j.jtbi.2012.02.021}, volume = {301}, year = {2012}, } @article{2849, author = {Edelsbrunner, Herbert and Strelkova, Nataliya}, journal = {Russian Mathematical Surveys}, number = {6}, pages = {1167 -- 1168}, publisher = {IOP Publishing Ltd.}, title = {{On the configuration space of Steiner minimal trees}}, doi = {10.1070/RM2012v067n06ABEH004820}, volume = {67}, year = {2012}, } @inproceedings{2888, abstract = {Formal verification aims to improve the quality of hardware and software by detecting errors before they do harm. At the basis of formal verification lies the logical notion of correctness, which purports to capture whether or not a circuit or program behaves as desired. We suggest that the boolean partition into correct and incorrect systems falls short of the practical need to assess the behavior of hardware and software in a more nuanced fashion against multiple criteria.}, author = {Henzinger, Thomas A}, booktitle = {Conference proceedings MODELS 2012}, location = {Innsbruck, Austria}, pages = {1 -- 2}, publisher = {Springer}, title = {{Quantitative reactive models}}, doi = {10.1007/978-3-642-33666-9_1}, volume = {7590}, year = {2012}, } @inproceedings{2890, abstract = {Systems are often specified using multiple requirements on their behavior. In practice, these requirements can be contradictory. The classical approach to specification, verification, and synthesis demands more detailed specifications that resolve any contradictions in the requirements. These detailed specifications are usually large, cumbersome, and hard to maintain or modify. In contrast, quantitative frameworks allow the formalization of the intuitive idea that what is desired is an implementation that comes "closest" to satisfying the mutually incompatible requirements, according to a measure of fit that can be defined by the requirements engineer. One flexible framework for quantifying how "well" an implementation satisfies a specification is offered by simulation distances that are parameterized by an error model. We introduce this framework, study its properties, and provide an algorithmic solution for the following quantitative synthesis question: given two (or more) behavioral requirements specified by possibly incompatible finite-state machines, and an error model, find the finite-state implementation that minimizes the maximal simulation distance to the given requirements. Furthermore, we generalize the framework to handle infinite alphabets (for example, realvalued domains). We also demonstrate how quantitative specifications based on simulation distances might lead to smaller and easier to modify specifications. Finally, we illustrate our approach using case studies on error correcting codes and scheduler synthesis.}, author = {Cerny, Pavol and Gopi, Sivakanth and Henzinger, Thomas A and Radhakrishna, Arjun and Totla, Nishant}, booktitle = {Proceedings of the tenth ACM international conference on Embedded software}, location = {Tampere, Finland}, pages = {53 -- 62}, publisher = {ACM}, title = {{Synthesis from incompatible specifications}}, doi = {10.1145/2380356.2380371}, year = {2012}, }