--- _id: '3270' abstract: - lang: eng text: 'The persistence diagram of a filtered simplicial com- plex is usually computed by reducing the boundary matrix of the complex. We introduce a simple op- timization technique: by processing the simplices of the complex in decreasing dimension, we can “kill” columns (i.e., set them to zero) without reducing them. This technique completely avoids reduction on roughly half of the columns. We demonstrate that this idea significantly improves the running time of the reduction algorithm in practice. We also give an output-sensitive complexity analysis for the new al- gorithm which yields to sub-cubic asymptotic bounds under certain assumptions.' author: - first_name: Chao full_name: Chen, Chao id: 3E92416E-F248-11E8-B48F-1D18A9856A87 last_name: Chen - first_name: Michael full_name: Kerber, Michael id: 36E4574A-F248-11E8-B48F-1D18A9856A87 last_name: Kerber orcid: 0000-0002-8030-9299 citation: ama: 'Chen C, Kerber M. Persistent homology computation with a twist. In: TU Dortmund; 2011:197-200.' apa: 'Chen, C., & Kerber, M. (2011). Persistent homology computation with a twist (pp. 197–200). Presented at the EuroCG: European Workshop on Computational Geometry, Morschach, Switzerland: TU Dortmund.' chicago: Chen, Chao, and Michael Kerber. “Persistent Homology Computation with a Twist,” 197–200. TU Dortmund, 2011. ieee: 'C. Chen and M. Kerber, “Persistent homology computation with a twist,” presented at the EuroCG: European Workshop on Computational Geometry, Morschach, Switzerland, 2011, pp. 197–200.' ista: 'Chen C, Kerber M. 2011. Persistent homology computation with a twist. EuroCG: European Workshop on Computational Geometry, 197–200.' mla: Chen, Chao, and Michael Kerber. Persistent Homology Computation with a Twist. TU Dortmund, 2011, pp. 197–200. short: C. Chen, M. Kerber, in:, TU Dortmund, 2011, pp. 197–200. conference: end_date: 2011-03-30 location: Morschach, Switzerland name: 'EuroCG: European Workshop on Computational Geometry' start_date: 2011-03-28 date_created: 2018-12-11T12:02:22Z date_published: 2011-01-01T00:00:00Z date_updated: 2021-01-12T07:42:17Z day: '01' department: - _id: HeEd language: - iso: eng month: '01' oa_version: None page: 197 - 200 publication_status: published publisher: TU Dortmund publist_id: '3376' quality_controlled: '1' status: public title: Persistent homology computation with a twist type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3298' abstract: - lang: eng text: We present a new algorithm for enforcing incompressibility for Smoothed Particle Hydrodynamics (SPH) by preserving uniform density across the domain. We propose a hybrid method that uses a Poisson solve on a coarse grid to enforce a divergence free velocity field, followed by a local density correction of the particles. This avoids typical grid artifacts and maintains the Lagrangian nature of SPH by directly transferring pressures onto particles. Our method can be easily integrated with existing SPH techniques such as the incompressible PCISPH method as well as weakly compressible SPH by adding an additional force term. We show that this hybrid method accelerates convergence towards uniform density and permits a significantly larger time step compared to earlier approaches while producing similar results. We demonstrate our approach in a variety of scenarios with significant pressure gradients such as splashing liquids. author: - first_name: Karthik full_name: Raveendran, Karthik last_name: Raveendran - first_name: Christopher J full_name: Wojtan, Christopher J id: 3C61F1D2-F248-11E8-B48F-1D18A9856A87 last_name: Wojtan orcid: 0000-0001-6646-5546 - first_name: Greg full_name: Turk, Greg last_name: Turk citation: ama: 'Raveendran K, Wojtan C, Turk G. Hybrid smoothed particle hydrodynamics. In: Spencer S, ed. ACM; 2011:33-42. doi:10.1145/2019406.2019411' apa: 'Raveendran, K., Wojtan, C., & Turk, G. (2011). Hybrid smoothed particle hydrodynamics. In S. Spencer (Ed.) (pp. 33–42). Presented at the SCA: ACM SIGGRAPH/Eurographics Symposium on Computer animation, Vancouver, Canada: ACM. https://doi.org/10.1145/2019406.2019411' chicago: Raveendran, Karthik, Chris Wojtan, and Greg Turk. “Hybrid Smoothed Particle Hydrodynamics.” edited by Stephen Spencer, 33–42. ACM, 2011. https://doi.org/10.1145/2019406.2019411. ieee: 'K. Raveendran, C. Wojtan, and G. Turk, “Hybrid smoothed particle hydrodynamics,” presented at the SCA: ACM SIGGRAPH/Eurographics Symposium on Computer animation, Vancouver, Canada, 2011, pp. 33–42.' ista: 'Raveendran K, Wojtan C, Turk G. 2011. Hybrid smoothed particle hydrodynamics. SCA: ACM SIGGRAPH/Eurographics Symposium on Computer animation, 33–42.' mla: Raveendran, Karthik, et al. Hybrid Smoothed Particle Hydrodynamics. Edited by Stephen Spencer, ACM, 2011, pp. 33–42, doi:10.1145/2019406.2019411. short: K. Raveendran, C. Wojtan, G. Turk, in:, S. Spencer (Ed.), ACM, 2011, pp. 33–42. conference: end_date: 2011-08-07 location: Vancouver, Canada name: 'SCA: ACM SIGGRAPH/Eurographics Symposium on Computer animation' start_date: 2011-08-05 date_created: 2018-12-11T12:02:32Z date_published: 2011-08-05T00:00:00Z date_updated: 2023-02-23T11:21:05Z day: '05' ddc: - '000' department: - _id: ChWo doi: 10.1145/2019406.2019411 editor: - first_name: Stephen full_name: Spencer, Stephen last_name: Spencer file: - access_level: open_access checksum: 6579d27709946e0eefbfa60a456b4913 content_type: application/pdf creator: system date_created: 2018-12-12T10:09:44Z date_updated: 2020-07-14T12:46:06Z file_id: '4769' file_name: IST-2016-598-v1+1_HybridSPH_Preprint.pdf file_size: 2536216 relation: main_file file_date_updated: 2020-07-14T12:46:06Z has_accepted_license: '1' language: - iso: eng month: '08' oa: 1 oa_version: Submitted Version page: 33 - 42 publication_status: published publisher: ACM publist_id: '3343' pubrep_id: '598' quality_controlled: '1' scopus_import: 1 status: public title: Hybrid smoothed particle hydrodynamics type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3297' abstract: - lang: eng text: "Animating detailed liquid surfaces has always been a challenge for computer graphics researchers and visual effects artists. Over the past few years, researchers in this field have focused on mesh-based surface tracking to synthesize extremely detailed liquid surfaces as efficiently as possible. This course provides a solid understanding of the steps required to create a fluid simulator with a mesh-based liquid surface.\r\n\r\nThe course begins with an overview of several existing liquid-surface-tracking techniques and the pros and cons of each method. Then it explains how to embed a triangle mesh into a finite-difference-based fluid simulator and describes several methods for allowing the liquid surface to merge together or break apart. The final section showcases the benefits and further applications of a mesh-based liquid surface, highlighting state-of-the-art methods for tracking colors and textures, maintaining liquid volume, preserving small surface features, and simulating realistic surface-tension waves." article_number: '8' author: - first_name: Christopher J full_name: Wojtan, Christopher J id: 3C61F1D2-F248-11E8-B48F-1D18A9856A87 last_name: Wojtan orcid: 0000-0001-6646-5546 - first_name: Matthias full_name: Müller Fischer, Matthias last_name: Müller Fischer - first_name: Tyson full_name: Brochu, Tyson last_name: Brochu citation: ama: 'Wojtan C, Müller Fischer M, Brochu T. Liquid simulation with mesh-based surface tracking. In: ACM; 2011. doi:10.1145/2037636.2037644' apa: 'Wojtan, C., Müller Fischer, M., & Brochu, T. (2011). Liquid simulation with mesh-based surface tracking. Presented at the SIGGRAPH: Special Interest Group on Computer Graphics and Interactive Techniques, Vancouver, BC, Canada: ACM. https://doi.org/10.1145/2037636.2037644' chicago: Wojtan, Chris, Matthias Müller Fischer, and Tyson Brochu. “Liquid Simulation with Mesh-Based Surface Tracking.” ACM, 2011. https://doi.org/10.1145/2037636.2037644. ieee: 'C. Wojtan, M. Müller Fischer, and T. Brochu, “Liquid simulation with mesh-based surface tracking,” presented at the SIGGRAPH: Special Interest Group on Computer Graphics and Interactive Techniques, Vancouver, BC, Canada, 2011.' ista: 'Wojtan C, Müller Fischer M, Brochu T. 2011. Liquid simulation with mesh-based surface tracking. SIGGRAPH: Special Interest Group on Computer Graphics and Interactive Techniques, 8.' mla: Wojtan, Chris, et al. Liquid Simulation with Mesh-Based Surface Tracking. 8, ACM, 2011, doi:10.1145/2037636.2037644. short: C. Wojtan, M. Müller Fischer, T. Brochu, in:, ACM, 2011. conference: end_date: 2011-08-11 location: Vancouver, BC, Canada name: 'SIGGRAPH: Special Interest Group on Computer Graphics and Interactive Techniques' start_date: 2011-08-07 date_created: 2018-12-11T12:02:31Z date_published: 2011-08-07T00:00:00Z date_updated: 2023-02-23T11:21:02Z day: '07' ddc: - '000' department: - _id: ChWo doi: 10.1145/2037636.2037644 file: - access_level: open_access checksum: 8d508ad7c82f50978acbaa4170ee0a75 content_type: application/pdf creator: system date_created: 2018-12-12T10:13:34Z date_updated: 2020-07-14T12:46:06Z file_id: '5018' file_name: IST-2016-599-v1+1_meshyFluidsCourseSIGGRAPH2011.pdf file_size: 34672096 relation: main_file file_date_updated: 2020-07-14T12:46:06Z has_accepted_license: '1' language: - iso: eng month: '08' oa: 1 oa_version: Published Version publication_status: published publisher: ACM publist_id: '3344' pubrep_id: '599' quality_controlled: '1' scopus_import: 1 status: public title: Liquid simulation with mesh-based surface tracking type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3290' abstract: - lang: eng text: 'Analysis of genomic data requires an efficient way to calculate likelihoods across very large numbers of loci. We describe a general method for finding the distribution of genealogies: we allow migration between demes, splitting of demes [as in the isolation-with-migration (IM) model], and recombination between linked loci. These processes are described by a set of linear recursions for the generating function of branch lengths. Under the infinite-sites model, the probability of any configuration of mutations can be found by differentiating this generating function. Such calculations are feasible for small numbers of sampled genomes: as an example, we show how the generating function can be derived explicitly for three genes under the two-deme IM model. This derivation is done automatically, using Mathematica. Given data from a large number of unlinked and nonrecombining blocks of sequence, these results can be used to find maximum-likelihood estimates of model parameters by tabulating the probabilities of all relevant mutational configurations and then multiplying across loci. The feasibility of the method is demonstrated by applying it to simulated data and to a data set previously analyzed by Wang and Hey (2010) consisting of 26,141 loci sampled from Drosophila simulans and D. melanogaster. Our results suggest that such likelihood calculations are scalable to genomic data as long as the numbers of sampled individuals and mutations per sequence block are small.' author: - first_name: Konrad full_name: Lohse, Konrad last_name: Lohse - first_name: Richard full_name: Harrison, Richard last_name: Harrison - first_name: Nicholas H full_name: Barton, Nicholas H id: 4880FE40-F248-11E8-B48F-1D18A9856A87 last_name: Barton orcid: 0000-0002-8548-5240 citation: ama: Lohse K, Harrison R, Barton NH. A general method for calculating likelihoods under the coalescent process. Genetics. 2011;189(3):977-987. doi:10.1534/genetics.111.129569 apa: Lohse, K., Harrison, R., & Barton, N. H. (2011). A general method for calculating likelihoods under the coalescent process. Genetics. Genetics Society of America. https://doi.org/10.1534/genetics.111.129569 chicago: Lohse, Konrad, Richard Harrison, and Nicholas H Barton. “A General Method for Calculating Likelihoods under the Coalescent Process.” Genetics. Genetics Society of America, 2011. https://doi.org/10.1534/genetics.111.129569. ieee: K. Lohse, R. Harrison, and N. H. Barton, “A general method for calculating likelihoods under the coalescent process,” Genetics, vol. 189, no. 3. Genetics Society of America, pp. 977–987, 2011. ista: Lohse K, Harrison R, Barton NH. 2011. A general method for calculating likelihoods under the coalescent process. Genetics. 189(3), 977–987. mla: Lohse, Konrad, et al. “A General Method for Calculating Likelihoods under the Coalescent Process.” Genetics, vol. 189, no. 3, Genetics Society of America, 2011, pp. 977–87, doi:10.1534/genetics.111.129569. short: K. Lohse, R. Harrison, N.H. Barton, Genetics 189 (2011) 977–987. date_created: 2018-12-11T12:02:29Z date_published: 2011-11-01T00:00:00Z date_updated: 2021-01-12T07:42:26Z day: '01' department: - _id: NiBa doi: 10.1534/genetics.111.129569 ec_funded: 1 intvolume: ' 189' issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3213358/ month: '11' oa: 1 oa_version: Submitted Version page: 977 - 987 project: - _id: 25B07788-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '250152' name: Limits to selection in biology and in evolutionary computation publication: Genetics publication_status: published publisher: Genetics Society of America publist_id: '3355' quality_controlled: '1' scopus_import: 1 status: public title: A general method for calculating likelihoods under the coalescent process type: journal_article user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 189 year: '2011' ... --- _id: '3312' abstract: - lang: eng text: We study the 3D reconstruction of plant roots from multiple 2D images. To meet the challenge caused by the delicate nature of thin branches, we make three innovations to cope with the sensitivity to image quality and calibration. First, we model the background as a harmonic function to improve the segmentation of the root in each 2D image. Second, we develop the concept of the regularized visual hull which reduces the effect of jittering and refraction by ensuring consistency with one 2D image. Third, we guarantee connectedness through adjustments to the 3D reconstruction that minimize global error. Our software is part of a biological phenotype/genotype study of agricultural root systems. It has been tested on more than 40 plant roots and results are promising in terms of reconstruction quality and efficiency. acknowledgement: This research is supported by the National Science Foundation (NSF) under grant DBI-0820624. article_number: '6126475' article_processing_charge: No author: - first_name: Ying full_name: Zheng, Ying last_name: Zheng - first_name: Steve full_name: Gu, Steve last_name: Gu - first_name: Herbert full_name: Edelsbrunner, Herbert id: 3FB178DA-F248-11E8-B48F-1D18A9856A87 last_name: Edelsbrunner orcid: 0000-0002-9823-6833 - first_name: Carlo full_name: Tomasi, Carlo last_name: Tomasi - first_name: Philip full_name: Benfey, Philip last_name: Benfey citation: ama: Zheng Y, Gu S, Edelsbrunner H, Tomasi C, Benfey P. Detailed Reconstruction of 3D Plant Root Shape. IEEE; 2011. doi:10.1109/ICCV.2011.6126475 apa: 'Zheng, Y., Gu, S., Edelsbrunner, H., Tomasi, C., & Benfey, P. (2011). Detailed reconstruction of 3D plant root shape. Proceedings of the IEEE International Conference on Computer Vision. Barcelona, Spain: IEEE. https://doi.org/10.1109/ICCV.2011.6126475' chicago: Zheng, Ying, Steve Gu, Herbert Edelsbrunner, Carlo Tomasi, and Philip Benfey. Detailed Reconstruction of 3D Plant Root Shape. Proceedings of the IEEE International Conference on Computer Vision. IEEE, 2011. https://doi.org/10.1109/ICCV.2011.6126475. ieee: Y. Zheng, S. Gu, H. Edelsbrunner, C. Tomasi, and P. Benfey, Detailed reconstruction of 3D plant root shape. IEEE, 2011. ista: Zheng Y, Gu S, Edelsbrunner H, Tomasi C, Benfey P. 2011. Detailed reconstruction of 3D plant root shape, IEEE,p. mla: Zheng, Ying, et al. “Detailed Reconstruction of 3D Plant Root Shape.” Proceedings of the IEEE International Conference on Computer Vision, 6126475, IEEE, 2011, doi:10.1109/ICCV.2011.6126475. short: Y. Zheng, S. Gu, H. Edelsbrunner, C. Tomasi, P. Benfey, Detailed Reconstruction of 3D Plant Root Shape, IEEE, 2011. conference: end_date: 2011-11-13 location: Barcelona, Spain name: 'ICCV: International Conference on Computer Vision' start_date: 2011-11-06 date_created: 2018-12-11T12:02:36Z date_published: 2011-12-31T00:00:00Z date_updated: 2020-07-14T23:03:43Z day: '31' ddc: - '000' department: - _id: HeEd doi: 10.1109/ICCV.2011.6126475 file: - access_level: open_access checksum: 30a33564b7b45a7ee31610898267fd0e content_type: application/pdf creator: system date_created: 2018-12-12T10:09:04Z date_updated: 2020-07-14T12:46:07Z file_id: '4727' file_name: IST-2016-541-v1+1_2011-P-07-RootReconstruction.pdf file_size: 5622728 relation: main_file file_date_updated: 2020-07-14T12:46:07Z has_accepted_license: '1' language: - iso: eng month: '12' oa: 1 oa_version: Submitted Version publication: Proceedings of the IEEE International Conference on Computer Vision publication_status: published publisher: IEEE publist_id: '3328' pubrep_id: '541' quality_controlled: '1' status: public title: Detailed reconstruction of 3D plant root shape type: conference_poster user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3313' abstract: - lang: eng text: Interpreting an image as a function on a compact sub- set of the Euclidean plane, we get its scale-space by diffu- sion, spreading the image over the entire plane. This gener- ates a 1-parameter family of functions alternatively defined as convolutions with a progressively wider Gaussian ker- nel. We prove that the corresponding 1-parameter family of persistence diagrams have norms that go rapidly to zero as time goes to infinity. This result rationalizes experimental observations about scale-space. We hope this will lead to targeted improvements of related computer vision methods. article_number: '6126271' author: - first_name: Chao full_name: Chen, Chao id: 3E92416E-F248-11E8-B48F-1D18A9856A87 last_name: Chen - first_name: Herbert full_name: Edelsbrunner, Herbert id: 3FB178DA-F248-11E8-B48F-1D18A9856A87 last_name: Edelsbrunner orcid: 0000-0002-9823-6833 citation: ama: 'Chen C, Edelsbrunner H. Diffusion runs low on persistence fast. In: Proceedings of the IEEE International Conference on Computer Vision. IEEE; 2011. doi:10.1109/ICCV.2011.6126271' apa: 'Chen, C., & Edelsbrunner, H. (2011). Diffusion runs low on persistence fast. In Proceedings of the IEEE International Conference on Computer Vision. Barcelona, Spain: IEEE. https://doi.org/10.1109/ICCV.2011.6126271' chicago: Chen, Chao, and Herbert Edelsbrunner. “Diffusion Runs Low on Persistence Fast.” In Proceedings of the IEEE International Conference on Computer Vision. IEEE, 2011. https://doi.org/10.1109/ICCV.2011.6126271. ieee: C. Chen and H. Edelsbrunner, “Diffusion runs low on persistence fast,” in Proceedings of the IEEE International Conference on Computer Vision, Barcelona, Spain, 2011. ista: 'Chen C, Edelsbrunner H. 2011. Diffusion runs low on persistence fast. Proceedings of the IEEE International Conference on Computer Vision. ICCV: International Conference on Computer Vision, 6126271.' mla: Chen, Chao, and Herbert Edelsbrunner. “Diffusion Runs Low on Persistence Fast.” Proceedings of the IEEE International Conference on Computer Vision, 6126271, IEEE, 2011, doi:10.1109/ICCV.2011.6126271. short: C. Chen, H. Edelsbrunner, in:, Proceedings of the IEEE International Conference on Computer Vision, IEEE, 2011. conference: end_date: 2011-11-13 location: Barcelona, Spain name: 'ICCV: International Conference on Computer Vision' start_date: 2011-11-06 date_created: 2018-12-11T12:02:37Z date_published: 2011-11-06T00:00:00Z date_updated: 2021-01-12T07:42:35Z day: '06' ddc: - '000' department: - _id: HeEd doi: 10.1109/ICCV.2011.6126271 file: - access_level: open_access checksum: 6984684081ba123808b344f9f2e64a8f content_type: application/pdf creator: system date_created: 2018-12-12T10:17:28Z date_updated: 2020-07-14T12:46:07Z file_id: '5282' file_name: IST-2016-540-v1+1_2011-P-08-RunEmpty.pdf file_size: 614050 relation: main_file file_date_updated: 2020-07-14T12:46:07Z has_accepted_license: '1' language: - iso: eng month: '11' oa: 1 oa_version: Submitted Version publication: Proceedings of the IEEE International Conference on Computer Vision publication_status: published publisher: IEEE publist_id: '3327' pubrep_id: '540' quality_controlled: '1' scopus_import: 1 status: public title: Diffusion runs low on persistence fast type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3311' abstract: - lang: eng text: Alpha shapes have been conceived in 1981 as an attempt to define the shape of a finite set of point in the plane. Since then, connections to diverse areas in the sciences and engineering have developed, including to pattern recognition, digital shape sampling and processing, and structural molecular biology. This survey begins with a historical account and discusses geometric, algorithmic, topological, and combinatorial aspects of alpha shapes in this sequence. article_processing_charge: No author: - first_name: Herbert full_name: Edelsbrunner, Herbert id: 3FB178DA-F248-11E8-B48F-1D18A9856A87 last_name: Edelsbrunner orcid: 0000-0002-9823-6833 citation: ama: 'Edelsbrunner H. Alpha shapes - a survey. In: van de Weygaert R, Vegter G, Ritzerveld J, Icke V, eds. Tessellations in the Sciences: Virtues, Techniques and Applications of Geometric Tilings. Springer.' apa: 'Edelsbrunner, H. (n.d.). Alpha shapes - a survey. In R. van de Weygaert, G. Vegter, J. Ritzerveld, & V. Icke (Eds.), Tessellations in the Sciences: Virtues, Techniques and Applications of Geometric Tilings. Springer.' chicago: 'Edelsbrunner, Herbert. “Alpha Shapes - a Survey.” In Tessellations in the Sciences: Virtues, Techniques and Applications of Geometric Tilings, edited by R van de Weygaert, G Vegter, J Ritzerveld, and V Icke. Springer, n.d.' ieee: 'H. Edelsbrunner, “Alpha shapes - a survey,” in Tessellations in the Sciences: Virtues, Techniques and Applications of Geometric Tilings, R. van de Weygaert, G. Vegter, J. Ritzerveld, and V. Icke, Eds. Springer.' ista: 'Edelsbrunner H.Alpha shapes - a survey. In: Tessellations in the Sciences: Virtues, Techniques and Applications of Geometric Tilings. .' mla: 'Edelsbrunner, Herbert. “Alpha Shapes - a Survey.” Tessellations in the Sciences: Virtues, Techniques and Applications of Geometric Tilings, edited by R van de Weygaert et al., Springer.' short: 'H. Edelsbrunner, in:, R. van de Weygaert, G. Vegter, J. Ritzerveld, V. Icke (Eds.), Tessellations in the Sciences: Virtues, Techniques and Applications of Geometric Tilings, Springer, n.d.' date_created: 2018-12-11T12:02:36Z date_published: 2011-12-31T00:00:00Z date_updated: 2022-05-24T07:56:30Z day: '31' ddc: - '510' department: - _id: HeEd editor: - first_name: R full_name: van de Weygaert, R last_name: van de Weygaert - first_name: G full_name: Vegter, G last_name: Vegter - first_name: J full_name: Ritzerveld, J last_name: Ritzerveld - first_name: V full_name: Icke, V last_name: Icke file: - access_level: open_access checksum: a592ea438351e7280eea993a7713ab8f content_type: application/pdf creator: dernst date_created: 2022-05-24T07:55:05Z date_updated: 2022-05-24T07:55:05Z file_id: '11408' file_name: 2010_AlphaShapes.pdf file_size: 475254 relation: main_file success: 1 file_date_updated: 2022-05-24T07:55:05Z has_accepted_license: '1' language: - iso: eng month: '12' oa: 1 oa_version: Submitted Version publication: 'Tessellations in the Sciences: Virtues, Techniques and Applications of Geometric Tilings' publication_status: inpress publisher: Springer publist_id: '3329' quality_controlled: '1' status: public title: Alpha shapes - a survey type: book_chapter user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3326' abstract: - lang: eng text: 'Weighted automata map input words to numerical values. Ap- plications of weighted automata include formal verification of quantitative properties, as well as text, speech, and image processing. A weighted au- tomaton is defined with respect to a semiring. For the tropical semiring, the weight of a run is the sum of the weights of the transitions taken along the run, and the value of a word is the minimal weight of an accepting run on it. In the 90’s, Krob studied the decidability of problems on rational series defined with respect to the tropical semiring. Rational series are strongly related to weighted automata, and Krob’s results apply to them. In par- ticular, it follows from Krob’s results that the universality problem (that is, deciding whether the values of all words are below some threshold) is decidable for weighted automata defined with respect to the tropical semir- ing with domain ∪ {∞}, and that the equality problem is undecidable when the domain is ∪ {∞}. In this paper we continue the study of the borders of decidability in weighted automata, describe alternative and direct proofs of the above results, and tighten them further. Unlike the proofs of Krob, which are algebraic in their nature, our proofs stay in the terrain of state machines, and the reduction is from the halting problem of a two-counter machine. This enables us to significantly simplify Krob’s reasoning, make the un- decidability result accessible to the automata-theoretic community, and strengthen it to apply already to a very simple class of automata: all the states are accepting, there are no initial nor final weights, and all the weights on the transitions are from the set {−1, 0, 1}. The fact we work directly with the automata enables us to tighten also the decidability re- sults and to show that the universality problem for weighted automata defined with respect to the tropical semiring with domain ∪ {∞}, and in fact even with domain ≥0 ∪ {∞}, is PSPACE-complete. Our results thus draw a sharper picture about the decidability of decision problems for weighted automata, in both the front of containment vs. universality and the front of the ∪ {∞} vs. the ∪ {∞} domains.' alternative_title: - LNCS article_processing_charge: No author: - first_name: Shaull full_name: Almagor, Shaull last_name: Almagor - first_name: Udi full_name: Boker, Udi id: 31E297B6-F248-11E8-B48F-1D18A9856A87 last_name: Boker - first_name: Orna full_name: Kupferman, Orna last_name: Kupferman citation: ama: 'Almagor S, Boker U, Kupferman O. What’s decidable about weighted automata . In: Vol 6996. Springer; 2011:482-491. doi:10.1007/978-3-642-24372-1_37' apa: 'Almagor, S., Boker, U., & Kupferman, O. (2011). What’s decidable about weighted automata (Vol. 6996, pp. 482–491). Presented at the ATVA: Automated Technology for Verification and Analysis, Taipei, Taiwan: Springer. https://doi.org/10.1007/978-3-642-24372-1_37' chicago: Almagor, Shaull, Udi Boker, and Orna Kupferman. “What’s Decidable about Weighted Automata ,” 6996:482–91. Springer, 2011. https://doi.org/10.1007/978-3-642-24372-1_37. ieee: 'S. Almagor, U. Boker, and O. Kupferman, “What’s decidable about weighted automata ,” presented at the ATVA: Automated Technology for Verification and Analysis, Taipei, Taiwan, 2011, vol. 6996, pp. 482–491.' ista: 'Almagor S, Boker U, Kupferman O. 2011. What’s decidable about weighted automata . ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 6996, 482–491.' mla: Almagor, Shaull, et al. What’s Decidable about Weighted Automata . Vol. 6996, Springer, 2011, pp. 482–91, doi:10.1007/978-3-642-24372-1_37. short: S. Almagor, U. Boker, O. Kupferman, in:, Springer, 2011, pp. 482–491. conference: end_date: 2011-10-14 location: Taipei, Taiwan name: 'ATVA: Automated Technology for Verification and Analysis' start_date: 2011-10-11 date_created: 2018-12-11T12:02:41Z date_published: 2011-10-14T00:00:00Z date_updated: 2021-01-12T07:42:40Z day: '14' ddc: - '000' department: - _id: ToHe doi: 10.1007/978-3-642-24372-1_37 file: - access_level: open_access checksum: a7ca08a2cb1b6925f4c18a3034ae5659 content_type: application/pdf creator: dernst date_created: 2020-05-19T16:08:32Z date_updated: 2020-07-14T12:46:07Z file_id: '7868' file_name: 2011_LNCS_Almagor.pdf file_size: 182309 relation: main_file file_date_updated: 2020-07-14T12:46:07Z has_accepted_license: '1' intvolume: ' 6996' language: - iso: eng month: '10' oa: 1 oa_version: Submitted Version page: 482 - 491 publication_status: published publisher: Springer publist_id: '3309' quality_controlled: '1' status: public title: 'What’s decidable about weighted automata ' type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 6996 year: '2011' ... --- _id: '3325' abstract: - lang: eng text: We introduce streaming data string transducers that map input data strings to output data strings in a single left-to-right pass in linear time. Data strings are (unbounded) sequences of data values, tagged with symbols from a finite set, over a potentially infinite data do- main that supports only the operations of equality and ordering. The transducer uses a finite set of states, a finite set of variables ranging over the data domain, and a finite set of variables ranging over data strings. At every step, it can make decisions based on the next in- put symbol, updating its state, remembering the input data value in its data variables, and updating data-string variables by concatenat- ing data-string variables and new symbols formed from data vari- ables, while avoiding duplication. We establish that the problems of checking functional equivalence of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by streaming acceptors over in- put/output data-strings, are in PSPACE. We identify a class of imperative and a class of functional pro- grams, manipulating lists of data items, which can be effectively translated to streaming data-string transducers. The imperative pro- grams dynamically modify a singly-linked heap by changing next- pointers of heap-nodes and by adding new nodes. The main re- striction specifies how the next-pointers can be used for traversal. We also identify an expressively equivalent fragment of functional programs that traverse a list using syntactically restricted recursive calls. Our results lead to algorithms for assertion checking and for checking functional equivalence of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse. article_processing_charge: No author: - first_name: Rajeev full_name: Alur, Rajeev last_name: Alur - first_name: Pavol full_name: Cerny, Pavol id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87 last_name: Cerny citation: ama: 'Alur R, Cerny P. Streaming transducers for algorithmic verification of single pass list processing programs. In: Vol 46. ACM; 2011:599-610. doi:10.1145/1926385.1926454' apa: 'Alur, R., & Cerny, P. (2011). Streaming transducers for algorithmic verification of single pass list processing programs (Vol. 46, pp. 599–610). Presented at the POPL: Principles of Programming Languages, Texas, USA: ACM. https://doi.org/10.1145/1926385.1926454' chicago: Alur, Rajeev, and Pavol Cerny. “Streaming Transducers for Algorithmic Verification of Single Pass List Processing Programs,” 46:599–610. ACM, 2011. https://doi.org/10.1145/1926385.1926454. ieee: 'R. Alur and P. Cerny, “Streaming transducers for algorithmic verification of single pass list processing programs,” presented at the POPL: Principles of Programming Languages, Texas, USA, 2011, vol. 46, no. 1, pp. 599–610.' ista: 'Alur R, Cerny P. 2011. Streaming transducers for algorithmic verification of single pass list processing programs. POPL: Principles of Programming Languages vol. 46, 599–610.' mla: Alur, Rajeev, and Pavol Cerny. Streaming Transducers for Algorithmic Verification of Single Pass List Processing Programs. Vol. 46, no. 1, ACM, 2011, pp. 599–610, doi:10.1145/1926385.1926454. short: R. Alur, P. Cerny, in:, ACM, 2011, pp. 599–610. conference: end_date: 2011-01-28 location: Texas, USA name: 'POPL: Principles of Programming Languages' start_date: 2011-01-26 date_created: 2018-12-11T12:02:41Z date_published: 2011-01-26T00:00:00Z date_updated: 2022-03-21T08:12:51Z day: '26' department: - _id: ToHe doi: 10.1145/1926385.1926454 intvolume: ' 46' issue: '1' language: - iso: eng month: '01' oa_version: None page: 599 - 610 publication_status: published publisher: ACM publist_id: '3310' quality_controlled: '1' scopus_import: '1' status: public title: Streaming transducers for algorithmic verification of single pass list processing programs type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 46 year: '2011' ... --- _id: '3324' abstract: - lang: eng text: 'Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program''s transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs.' alternative_title: - LNCS author: - first_name: Ruzica full_name: Piskac, Ruzica last_name: Piskac - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies citation: ama: 'Piskac R, Wies T. Decision procedures for automating termination proofs. In: Jhala R, Schmidt D, eds. Vol 6538. Springer; 2011:371-386. doi:10.1007/978-3-642-18275-4_26' apa: 'Piskac, R., & Wies, T. (2011). Decision procedures for automating termination proofs. In R. Jhala & D. Schmidt (Eds.) (Vol. 6538, pp. 371–386). Presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA: Springer. https://doi.org/10.1007/978-3-642-18275-4_26' chicago: Piskac, Ruzica, and Thomas Wies. “Decision Procedures for Automating Termination Proofs.” edited by Ranjit Jhala and David Schmidt, 6538:371–86. Springer, 2011. https://doi.org/10.1007/978-3-642-18275-4_26. ieee: 'R. Piskac and T. Wies, “Decision procedures for automating termination proofs,” presented at the VMCAI: Verification Model Checking and Abstract Interpretation, Texas, USA, 2011, vol. 6538, pp. 371–386.' ista: 'Piskac R, Wies T. 2011. Decision procedures for automating termination proofs. VMCAI: Verification Model Checking and Abstract Interpretation, LNCS, vol. 6538, 371–386.' mla: Piskac, Ruzica, and Thomas Wies. Decision Procedures for Automating Termination Proofs. Edited by Ranjit Jhala and David Schmidt, vol. 6538, Springer, 2011, pp. 371–86, doi:10.1007/978-3-642-18275-4_26. short: R. Piskac, T. Wies, in:, R. Jhala, D. Schmidt (Eds.), Springer, 2011, pp. 371–386. conference: end_date: 2011-01-25 location: Texas, USA name: 'VMCAI: Verification Model Checking and Abstract Interpretation' start_date: 2011-01-23 date_created: 2018-12-11T12:02:40Z date_published: 2011-01-01T00:00:00Z date_updated: 2021-01-12T07:42:39Z day: '01' department: - _id: ToHe doi: 10.1007/978-3-642-18275-4_26 editor: - first_name: Ranjit full_name: Jhala, Ranjit last_name: Jhala - first_name: David full_name: Schmidt, David last_name: Schmidt intvolume: ' 6538' language: - iso: eng main_file_link: - open_access: '1' url: https://infoscience.epfl.ch/record/170697/ month: '01' oa: 1 oa_version: Submitted Version page: 371 - 386 publication_status: published publisher: Springer publist_id: '3311' quality_controlled: '1' scopus_import: 1 status: public title: Decision procedures for automating termination proofs type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6538 year: '2011' ...