TY - CHAP AB - Primary neuronal cell culture preparations are widely used to investigate synaptic functions. This chapter describes a detailed protocol for the preparation of a neuronal cell culture in which giant calyx-type synaptic terminals are formed. This chapter also presents detailed protocols for utilizing the main technical advantages provided by such a preparation, namely, labeling and imaging of synaptic organelles and electrophysiological recordings directly from presynaptic terminals. AU - Dimitrov, Dimitar AU - Guillaud, Laurent AU - Eguchi, Kohgaku AU - Takahashi, Tomoyuki ED - Skaper, Stephen D. ID - 562 T2 - Neurotrophic Factors TI - Culture of mouse giant central nervous system synapses and application for imaging and electrophysiological analyses VL - 1727 ER - TY - CHAP AB - Graph-based games are an important tool in computer science. They have applications in synthesis, verification, refinement, and far beyond. We review graphbased games with objectives on infinite plays. We give definitions and algorithms to solve the games and to give a winning strategy. The objectives we consider are mostly Boolean, but we also look at quantitative graph-based games and their objectives. Synthesis aims to turn temporal logic specifications into correct reactive systems. We explain the reduction of synthesis to graph-based games (or equivalently tree automata) using synthesis of LTL specifications as an example. We treat the classical approach that uses determinization of parity automata and more modern approaches. AU - Bloem, Roderick AU - Chatterjee, Krishnendu AU - Jobstmann, Barbara ED - Henzinger, Thomas A ED - Clarke, Edmund M. ED - Veith, Helmut ED - Bloem, Roderick ID - 59 SN - 978-3-319-10574-1 T2 - Handbook of Model Checking TI - Graph games and reactive synthesis ER - TY - CHAP AB - Model checking is a computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems. Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry. This chapter is an introduction and short survey of model checking. The chapter aims to motivate and link the individual chapters of the handbook, and to provide context for readers who are not familiar with model checking. AU - Clarke, Edmund AU - Henzinger, Thomas A AU - Veith, Helmut ED - Henzinger, Thomas A ID - 60 T2 - Handbook of Model Checking TI - Introduction to model checking ER - TY - CHAP AB - We prove that there is no strongly regular graph (SRG) with parameters (460; 153; 32; 60). The proof is based on a recent lower bound on the number of 4-cliques in a SRG and some applications of Euclidean representation of SRGs. AU - Bondarenko, Andriy AU - Mellit, Anton AU - Prymak, Andriy AU - Radchenko, Danylo AU - Viazovska, Maryna ID - 61 T2 - Contemporary Computational Mathematics TI - There is no strongly regular graph with parameters (460; 153; 32; 60) ER - TY - JOUR AB - Blood platelets are critical for hemostasis and thrombosis, but also play diverse roles during immune responses. We have recently reported that platelets migrate at sites of infection in vitro and in vivo. Importantly, platelets use their ability to migrate to collect and bundle fibrin (ogen)-bound bacteria accomplishing efficient intravascular bacterial trapping. Here, we describe a method that allows analyzing platelet migration in vitro, focusing on their ability to collect bacteria and trap bacteria under flow. AU - Fan, Shuxia AU - Lorenz, Michael AU - Massberg, Steffen AU - Gärtner, Florian R ID - 6354 IS - 18 JF - Bio-Protocol KW - Platelets KW - Cell migration KW - Bacteria KW - Shear flow KW - Fibrinogen KW - E. coli SN - 2331-8325 TI - Platelet migration and bacterial trapping assay under flow VL - 8 ER -