Showing 1–15 of 15 results for author: Gazda, M

Generative Adversarial Networks in Ultrasound Imaging: Extending Field of View Beyond Conventional Limits

Authors: Matej Gazda, Samuel Kadoury, Jakub Gazda, Peter Drotar

Abstract: Transthoracic Echocardiography (TTE) is a fundamental, non-invasive diagnostic tool in cardiovascular medicine, enabling detailed visualization of cardiac structures crucial for diagnosing various heart conditions. Despite its widespread use, TTE ultrasound imaging faces inherent limitations, notably the trade-off between field of view (FoV) and resolution. This paper introduces a novel applicatio… ▽ More Transthoracic Echocardiography (TTE) is a fundamental, non-invasive diagnostic tool in cardiovascular medicine, enabling detailed visualization of cardiac structures crucial for diagnosing various heart conditions. Despite its widespread use, TTE ultrasound imaging faces inherent limitations, notably the trade-off between field of view (FoV) and resolution. This paper introduces a novel application of conditional Generative Adversarial Networks (cGANs), specifically designed to extend the FoV in TTE ultrasound imaging while maintaining high resolution. Our proposed cGAN architecture, termed echoGAN, demonstrates the capability to generate realistic anatomical structures through outpainting, effectively broadening the viewable area in medical imaging. This advancement has the potential to enhance both automatic and manual ultrasound navigation, offering a more comprehensive view that could significantly reduce the learning curve associated with ultrasound imaging and aid in more accurate diagnoses. The results confirm that echoGAN reliably reproduce detailed cardiac features, thereby promising a significant step forward in the field of non-invasive cardiac naviagation and diagnostics. △ Less

Submitted 31 May, 2024; originally announced May 2024.

End-to-end Deformable Attention Graph Neural Network for Single-view Liver Mesh Reconstruction

Authors: Matej Gazda, Peter Drotar, Liset Vazquez Romaguera, Samuel Kadoury

Abstract: Intensity modulated radiotherapy (IMRT) is one of the most common modalities for treating cancer patients. One of the biggest challenges is precise treatment delivery that accounts for varying motion patterns originating from free-breathing. Currently, image-guided solutions for IMRT is limited to 2D guidance due to the complexity of 3D tracking solutions. We propose a novel end-to-end attention g… ▽ More Intensity modulated radiotherapy (IMRT) is one of the most common modalities for treating cancer patients. One of the biggest challenges is precise treatment delivery that accounts for varying motion patterns originating from free-breathing. Currently, image-guided solutions for IMRT is limited to 2D guidance due to the complexity of 3D tracking solutions. We propose a novel end-to-end attention graph neural network model that generates in real-time a triangular shape of the liver based on a reference segmentation obtained at the preoperative phase and a 2D MRI coronal slice taken during the treatment. Graph neural networks work directly with graph data and can capture hidden patterns in non-Euclidean domains. Furthermore, contrary to existing methods, it produces the shape entirely in a mesh structure and correctly infers mesh shape and position based on a surrogate image. We define two on-the-fly approaches to make the correspondence of liver mesh vertices with 2D images obtained during treatment. Furthermore, we introduce a novel task-specific identity loss to constrain the deformation of the liver in the graph neural network to limit phenomenons such as flying vertices or mesh holes. The proposed method achieves results with an average error of 3.06 +- 0.7 mm and Chamfer distance with L2 norm of 63.14 +- 27.28. △ Less

Submitted 13 March, 2023; originally announced March 2023.

Comments: Copyright 2023 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works

Biomedical image analysis competitions: The state of current participation practice

Authors: Matthias Eisenmann, Annika Reinke, Vivienn Weru, Minu Dietlinde Tizabi, Fabian Isensee, Tim J. Adler, Patrick Godau, Veronika Cheplygina, Michal Kozubek, Sharib Ali, Anubha Gupta, Jan Kybic, Alison Noble, Carlos Ortiz de Solórzano, Samiksha Pachade, Caroline Petitjean, Daniel Sage, Donglai Wei, Elizabeth Wilden, Deepak Alapatt, Vincent Andrearczyk, Ujjwal Baid, Spyridon Bakas, Niranjan Balu, Sophia Bano , et al. (331 additional authors not shown)

Abstract: The number of international benchmarking competitions is steadily increasing in various fields of machine learning (ML) research and practice. So far, however, little is known about the common practice as well as bottlenecks faced by the community in tackling the research questions posed. To shed light on the status quo of algorithm development in the specific field of biomedical imaging analysis,… ▽ More The number of international benchmarking competitions is steadily increasing in various fields of machine learning (ML) research and practice. So far, however, little is known about the common practice as well as bottlenecks faced by the community in tackling the research questions posed. To shed light on the status quo of algorithm development in the specific field of biomedical imaging analysis, we designed an international survey that was issued to all participants of challenges conducted in conjunction with the IEEE ISBI 2021 and MICCAI 2021 conferences (80 competitions in total). The survey covered participants' expertise and working environments, their chosen strategies, as well as algorithm characteristics. A median of 72% challenge participants took part in the survey. According to our results, knowledge exchange was the primary incentive (70%) for participation, while the reception of prize money played only a minor role (16%). While a median of 80 working hours was spent on method development, a large portion of participants stated that they did not have enough time for method development (32%). 25% perceived the infrastructure to be a bottleneck. Overall, 94% of all solutions were deep learning-based. Of these, 84% were based on standard architectures. 43% of the respondents reported that the data samples (e.g., images) were too large to be processed at once. This was most commonly addressed by patch-based training (69%), downsampling (37%), and solving 3D analysis tasks as a series of 2D tasks. K-fold cross-validation on the training set was performed by only 37% of the participants and only 50% of the participants performed ensembling based on multiple identical models (61%) or heterogeneous models (39%). 48% of the respondents applied postprocessing steps. △ Less

Submitted 12 September, 2023; v1 submitted 16 December, 2022; originally announced December 2022.

What is in a Name: Defining -High Entropy- Oxides

Authors: Matthew Brahlek, Maria Gazda, Veerle Keppens, Alessandro R. Mazza, Scott J. McCormack, Aleksandra Mielewczyk-Gryń, Brianna Musico, Katharine Page, Christina Rost, Susan B. Sinnott, Cormac Toher, Thomas Z. Ward, Ayako Yamamoto

Abstract: High entropy oxides are emerging as an exciting new avenue to design highly tailored functional behaviors that have no traditional counterparts. Study and application of these materials are bringing together scientists and engineers from physics, chemistry, and materials science. The diversity of each of these disciplines comes with perspectives and jargon that may be confusing to those outside of… ▽ More High entropy oxides are emerging as an exciting new avenue to design highly tailored functional behaviors that have no traditional counterparts. Study and application of these materials are bringing together scientists and engineers from physics, chemistry, and materials science. The diversity of each of these disciplines comes with perspectives and jargon that may be confusing to those outside of the individual fields, which can result in miscommunication of important aspects of research. In this perspective, we provide examples of research and characterization taken from these different fields to provide a framework for classifying the differences between compositionally complex oxides, high entropy oxides, and entropy stabilized oxides, which is intended to bring a common language to this emerging area. We highlight the critical importance of understanding a materials crystallinity, composition, and mixing length scales in determining its true definition. △ Less

Submitted 4 November, 2022; v1 submitted 26 August, 2022; originally announced August 2022.

Self-supervised deep convolutional neural network for chest X-ray classification

Authors: Matej Gazda, Jakub Gazda, Jan Plavka, Peter Drotar

Abstract: Chest radiography is a relatively cheap, widely available medical procedure that conveys key information for making diagnostic decisions. Chest X-rays are almost always used in the diagnosis of respiratory diseases such as pneumonia or the recent COVID-19. In this paper, we propose a self-supervised deep neural network that is pretrained on an unlabeled chest X-ray dataset. The learned representat… ▽ More Chest radiography is a relatively cheap, widely available medical procedure that conveys key information for making diagnostic decisions. Chest X-rays are almost always used in the diagnosis of respiratory diseases such as pneumonia or the recent COVID-19. In this paper, we propose a self-supervised deep neural network that is pretrained on an unlabeled chest X-ray dataset. The learned representations are transferred to downstream task - the classification of respiratory diseases. The results obtained on four public datasets show that our approach yields competitive results without requiring large amounts of labeled training data. △ Less

Submitted 4 November, 2021; v1 submitted 4 March, 2021; originally announced March 2021.

Comments: The work was published by IEEE Access. DOI: 10.1109/ACCESS.2021.3125324

Conformance Relations and Hyperproperties for Do** Detection in Time and Space

Authors: Sebastian Biewer, Rayna Dimitrova, Michael Fries, Maciej Gazda, Thomas Heinze, Holger Hermanns, Mohammad Reza Mousavi

Abstract: We present a novel and generalised notion of do** cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, a… ▽ More We present a novel and generalised notion of do** cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for do** detection and apply our definitions to a case study concerning diesel emission tests. △ Less

Submitted 17 January, 2022; v1 submitted 7 December, 2020; originally announced December 2020.

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (January 19, 2022) lmcs:6963

Pressure effects on the electronic structure and superconductivity of (TaNb)$_{0.67}$(HfZrTi)$_{0.33}$ high entropy alloy

Authors: K. Jasiewicz, B. Wiendlocha, K. Górnicka, K. Gofryk, M. Gazda, T. Klimczuk, J. Tobola

Abstract: Effects of pressure on the electronic structure, electron-phonon interaction, and superconductivity of the high entropy alloy (TaNb)$_{0.67}$(HfZrTi)$_{0.33}$ are studied in the pressure range 0 - 100 GPa. The electronic structure is calculated using the Korringa-Kohn-Rostoker method with the coherent potential approximation. Effects of pressure on the lattice dynamics are simulated using the Deby… ▽ More Effects of pressure on the electronic structure, electron-phonon interaction, and superconductivity of the high entropy alloy (TaNb)$_{0.67}$(HfZrTi)$_{0.33}$ are studied in the pressure range 0 - 100 GPa. The electronic structure is calculated using the Korringa-Kohn-Rostoker method with the coherent potential approximation. Effects of pressure on the lattice dynamics are simulated using the Debye-Grüneisen model and the Grüneisen parameter at ambient conditions. In addition, the Debye temperature and Sommerfeld electronic heat capacity coefficient were experimentally determined. The electron-phonon coupling parameter $λ$ is calculated using the McMillan-Hopfield parameters and computed within the rigid muffin tin approximation. We find, that the system undergoes the Lifshitz transition, as one of the bands crosses the Fermi level at elevated pressures. The electron-phonon coupling parameter $λ$ decreases above 10 GPa. The calculated superconducting $T_c$ increases up to 40 - 50 GPa and, later, is stabilized at the larger value than for the ambient conditions, in agreement with the experimental findings. Our results show that the experimentally observed evolution of $T_c$ with pressure in (TaNb)$_{0.67}$(HfZrTi)$_{0.33}$ can be well explained by the classical electron-phonon mechanism. △ Less

Submitted 18 October, 2019; originally announced October 2019.

Comments: 19 pages, 20 figures including Supplemental Material, accepted in PRB

Distinguishing between Communicating Transactions

Authors: Vasileios Koutavas, Maciej Gazda, Matthew Hennessy

Abstract: Communicating transactions is a form of distributed, non-isolated transactions which provides a simple construct for building concurrent systems. In this paper we develop a logical framework to express properties of the observable behaviour of such systems. This comprises three nominal modal logics which share standard communication modalities but have distinct past and future modalities involving… ▽ More Communicating transactions is a form of distributed, non-isolated transactions which provides a simple construct for building concurrent systems. In this paper we develop a logical framework to express properties of the observable behaviour of such systems. This comprises three nominal modal logics which share standard communication modalities but have distinct past and future modalities involving transactional commits. All three logics have the same distinguishing power over systems because their associated weak bisimulations coincide with contextual equivalence. Furthermore, they are equally expressive because there are semantics-preserving translations between their formulae. Using the logics we can clearly exhibit subtle example inequivalences. This work presents the first property logics for non-isolated transactions. △ Less

Submitted 12 January, 2018; v1 submitted 9 March, 2017; originally announced March 2017.

Comments: Published in Information and Computation. This is author's final version

Improvement in Small Progress Measures

Authors: Maciej Gazda, Tim A. C. Willemse

Abstract: Small Progress Measures is one of the classical parity game solving algorithms. For games with n vertices, m edges and d different priorities, the original algorithm computes the winning regions and a winning strategy for one of the players in O(dm.(n/floor(d/2))^floor(d/2)) time. Computing a winning strategy for the other player requires a re-run of the algorithm on that player's winning region,… ▽ More Small Progress Measures is one of the classical parity game solving algorithms. For games with n vertices, m edges and d different priorities, the original algorithm computes the winning regions and a winning strategy for one of the players in O(dm.(n/floor(d/2))^floor(d/2)) time. Computing a winning strategy for the other player requires a re-run of the algorithm on that player's winning region, thus increasing the runtime complexity to O(dm.(n/ceil(d/2))^ceil(d/2)) for computing the winning regions and winning strategies for both players. We modify the algorithm so that it derives the winning strategy for both players in one pass. This reduces the upper bound on strategy derivation for SPM to O(dm.(n/floor(d/2))^floor(d/2)). At the basis of our modification is a novel operational interpretation of the least progress measure that we provide. △ Less

Submitted 23 September, 2015; originally announced September 2015.

Comments: In Proceedings GandALF 2015, arXiv:1509.06858

Journal ref: EPTCS 193, 2015, pp. 158-171

Pressure effects on the superconductivity of HfPd2Al Heusler compound: Experimental and theoretical study

Authors: B. Wiendlocha, M. J. Winiarski, M. Muras, C. Zvoriste-Walters, J. -C. Griveau, S. Heathman, M. Gazda, T. Klimczuk

Abstract: Polycrystalline HfPd2Al has been synthesized using the arc-melting method and studied under ambient pressure conditions by x-ray diffraction from room temperature up to 450^oC. High pressure x-ray diffraction up to 23 GPa was also performed using Diacell-type membrane diamond anvil cells. The estimated linear thermal expansion coefficient was found to be α = 1.40(3)x10^{-5} K^{-1}, and the bulk mo… ▽ More Polycrystalline HfPd2Al has been synthesized using the arc-melting method and studied under ambient pressure conditions by x-ray diffraction from room temperature up to 450^oC. High pressure x-ray diffraction up to 23 GPa was also performed using Diacell-type membrane diamond anvil cells. The estimated linear thermal expansion coefficient was found to be α = 1.40(3)x10^{-5} K^{-1}, and the bulk modulus derived from the fit to the 3rd order Birch-Murnaghan EOS (BMEOS) is B0 = 97(2) GPa. Resistivity studies under applied pressure (p < 7.49 GPa) showed a linear decrease of superconducting critical temperature with increasing pressure and the slope dTc/dp = -0.13(1) K GPa^{-1}. The same behavior is observed for the electron-phonon coupling constant {λ_{ep}}(p) that changes from 0.67 to 0.6, estimated for p = 0.05 GPa and 7.49 GPa, respectively. First principles electronic structure and phonon calculation results are presented and used to estimate the magnitude of electron-phonon interaction {λ_{ep}} and its evolution with pressure. Theoretical results explain the experimentally observed decrease in Tc due to considerable lattice stiffening. △ Less

Submitted 19 January, 2015; v1 submitted 23 December, 2014; originally announced December 2014.

Comments: 10 figures

Journal ref: Phys. Rev. B 91, 024509 (2015)

Strategy Derivation for Small Progress Measures

Authors: Maciej Gazda, Tim A. C. Willemse

Abstract: Small Progress Measures is one of the most efficient parity game solving algorithms. The original algorithm provides the full solution (winning regions and strategies) in $O(dm \cdot (n/\lceil d / 2 \rceil)^{\lceil d/2 \rceil})$ time, and requires a re-run of the algorithm on one of the winning regions. We provide a novel operational interpretation of progress measures, and modify the algorithm so… ▽ More Small Progress Measures is one of the most efficient parity game solving algorithms. The original algorithm provides the full solution (winning regions and strategies) in $O(dm \cdot (n/\lceil d / 2 \rceil)^{\lceil d/2 \rceil})$ time, and requires a re-run of the algorithm on one of the winning regions. We provide a novel operational interpretation of progress measures, and modify the algorithm so that it derives the winning strategies for both players in one pass. This reduces the upper bound on strategy derivation for SPM to $O(dm \cdot (n/\lfloor d / 2 \rfloor)^{\lfloor d/2 \rfloor})$. △ Less

Submitted 19 May, 2015; v1 submitted 8 July, 2014; originally announced July 2014.

Comments: polished the text

Zielonka's Recursive Algorithm: dull, weak and solitaire games and tighter bounds

Authors: Maciej Gazda, Tim A. C. Willemse

Abstract: Dull, weak and nested solitaire games are important classes of parity games, capturing, among others, alternation-free mu-calculus and ECTL* model checking problems. These classes can be solved in polynomial time using dedicated algorithms. We investigate the complexity of Zielonka's Recursive algorithm for solving these special games, showing that the algorithm runs in O(d (n + m)) on weak games,… ▽ More Dull, weak and nested solitaire games are important classes of parity games, capturing, among others, alternation-free mu-calculus and ECTL* model checking problems. These classes can be solved in polynomial time using dedicated algorithms. We investigate the complexity of Zielonka's Recursive algorithm for solving these special games, showing that the algorithm runs in O(d (n + m)) on weak games, and, somewhat surprisingly, that it requires exponential time to solve dull games and (nested) solitaire games. For the latter classes, we provide a family of games G, allowing us to establish a lower bound of 2^(n/3). We show that an optimisation of Zielonka's algorithm permits solving games from all three classes in polynomial time. Moreover, we show that there is a family of (non-special) games M that permits us to establish a lower bound of 2^(n/3), improving on the previous lower bound for the algorithm. △ Less

Submitted 16 July, 2013; originally announced July 2013.

Comments: In Proceedings GandALF 2013, arXiv:1307.4162

Journal ref: EPTCS 119, 2013, pp. 7-20

Expressiveness and Completeness in Abstraction

Authors: Maciej Gazda, Tim A. C. Willemse

Abstract: We study two notions of expressiveness, which have appeared in abstraction theory for model checking, and find them incomparable in general. In particular, we show that according to the most widely used notion, the class of Kripke Modal Transition Systems is strictly less expressive than the class of Generalised Kripke Modal Transition Systems (a generalised variant of Kripke Modal Transition Syst… ▽ More We study two notions of expressiveness, which have appeared in abstraction theory for model checking, and find them incomparable in general. In particular, we show that according to the most widely used notion, the class of Kripke Modal Transition Systems is strictly less expressive than the class of Generalised Kripke Modal Transition Systems (a generalised variant of Kripke Modal Transition Systems equipped with hypertransitions). Furthermore, we investigate the ability of an abstraction framework to prove a formula with a finite abstract model, a property known as completeness. We address the issue of completeness from a general perspective: the way it depends on certain abstraction parameters, as well as its relationship with expressiveness. △ Less

Submitted 13 August, 2012; originally announced August 2012.

Comments: In Proceedings EXPRESS/SOS 2012, arXiv:1208.2440

Journal ref: EPTCS 89, 2012, pp. 49-64

Congruence from the Operator's Point of View: Compositionality Requirements on Process Semantics

Authors: Maciej Gazda, Wan Fokkink

Abstract: One of the basic sanity properties of a behavioural semantics is that it constitutes a congruence with respect to standard process operators. This issue has been traditionally addressed by the development of rule formats for transition system specifications that define process algebras. In this paper we suggest a novel, orthogonal approach. Namely, we focus on a number of process operators, an… ▽ More One of the basic sanity properties of a behavioural semantics is that it constitutes a congruence with respect to standard process operators. This issue has been traditionally addressed by the development of rule formats for transition system specifications that define process algebras. In this paper we suggest a novel, orthogonal approach. Namely, we focus on a number of process operators, and for each of them attempt to find the widest possible class of congruences. To this end, we impose restrictions on sublanguages of Hennessy-Milner logic, so that a semantics whose modal characterization satisfies a given criterion is guaranteed to be a congruence with respect to the operator in question. We investigate action prefix, alternative composition, two restriction operators, and parallel composition. △ Less

Submitted 12 August, 2010; originally announced August 2010.

Comments: In Proceedings SOS 2010, arXiv:1008.1906

Journal ref: EPTCS 32, 2010, pp. 15-25

Modal Logic and the Approximation Induction Principle

Authors: Maciej Gazda, Wan Fokkink

Abstract: We prove a compactness theorem in the context of Hennessy-Milner logic. It is used to derive a sufficient condition on modal characterizations for the Approximation Induction Principle to be sound modulo the corresponding process equivalence. We show that this condition is necessary when the equivalence in question is compositional with respect to the projection operators. We prove a compactness theorem in the context of Hennessy-Milner logic. It is used to derive a sufficient condition on modal characterizations for the Approximation Induction Principle to be sound modulo the corresponding process equivalence. We show that this condition is necessary when the equivalence in question is compositional with respect to the projection operators. △ Less

Submitted 10 November, 2009; originally announced November 2009.

Journal ref: EPTCS 8, 2009, pp. 41-50